MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frxp Structured version   Visualization version   GIF version

Theorem frxp 7437
Description: A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.)
Hypothesis
Ref Expression
frxp.1 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
Assertion
Ref Expression
frxp ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦)

Proof of Theorem frxp
Dummy variables 𝑎 𝑏 𝑐 𝑠 𝑣 𝑤 𝑧 𝑑 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssn0 4118 . . . . . . . . 9 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2 xpnz 5694 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
32biimpri 218 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
43simprd 477 . . . . . . . . 9 ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
51, 4syl 17 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6 dmxp 5482 . . . . . . . . . 10 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7 dmss 5461 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8 sseq2 3774 . . . . . . . . . . 11 (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠𝐴))
97, 8syl5ib 234 . . . . . . . . . 10 (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
106, 9syl 17 . . . . . . . . 9 (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
1110impcom 394 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠𝐴)
125, 11syldan 571 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠𝐴)
13 relxp 5266 . . . . . . . . . . 11 Rel (𝐴 × 𝐵)
14 relss 5346 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
1513, 14mpi 20 . . . . . . . . . 10 (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16 reldm0 5481 . . . . . . . . . 10 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1715, 16syl 17 . . . . . . . . 9 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1817necon3bid 2986 . . . . . . . 8 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
1918biimpa 462 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
2012, 19jca 495 . . . . . 6 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅))
21 df-fr 5208 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎))
22 vex 3352 . . . . . . . . 9 𝑠 ∈ V
2322dmex 7245 . . . . . . . 8 dom 𝑠 ∈ V
24 sseq1 3773 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣𝐴 ↔ dom 𝑠𝐴))
25 neeq1 3004 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
2624, 25anbi12d 608 . . . . . . . . 9 (𝑣 = dom 𝑠 → ((𝑣𝐴𝑣 ≠ ∅) ↔ (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅)))
27 raleq 3286 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (∀𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2827rexeqbi1dv 3295 . . . . . . . . 9 (𝑣 = dom 𝑠 → (∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2926, 28imbi12d 333 . . . . . . . 8 (𝑣 = dom 𝑠 → (((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
3023, 29spcv 3448 . . . . . . 7 (∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3121, 30sylbi 207 . . . . . 6 (𝑅 Fr 𝐴 → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3220, 31syl5 34 . . . . 5 (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3332adantr 466 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34 imassrn 5618 . . . . . . . . . . . . . . 15 (𝑠 “ {𝑎}) ⊆ ran 𝑠
35 xpeq0 5695 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
3635biimpri 218 . . . . . . . . . . . . . . . . . . 19 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
3736orcs 855 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38 sseq2 3774 . . . . . . . . . . . . . . . . . . 19 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39 ss0 4116 . . . . . . . . . . . . . . . . . . 19 (𝑠 ⊆ ∅ → 𝑠 = ∅)
4038, 39syl6bi 243 . . . . . . . . . . . . . . . . . 18 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
4137, 40syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42 rneq 5489 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → ran 𝑠 = ran ∅)
43 rn0 5515 . . . . . . . . . . . . . . . . . . 19 ran ∅ = ∅
44 0ss 4114 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝐵
4543, 44eqsstri 3782 . . . . . . . . . . . . . . . . . 18 ran ∅ ⊆ 𝐵
4642, 45syl6eqss 3802 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → ran 𝑠𝐵)
4741, 46syl6 35 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
48 rnxp 5705 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49 rnss 5492 . . . . . . . . . . . . . . . . . 18 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50 sseq2 3774 . . . . . . . . . . . . . . . . . 18 (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠𝐵))
5149, 50syl5ib 234 . . . . . . . . . . . . . . . . 17 (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5248, 51syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5347, 52pm2.61ine 3025 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵)
5434, 53syl5ss 3761 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55 vex 3352 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
5655eldm 5459 . . . . . . . . . . . . . . 15 (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57 vex 3352 . . . . . . . . . . . . . . . . . . 19 𝑏 ∈ V
5855, 57elimasn 5631 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59 df-br 4785 . . . . . . . . . . . . . . . . . 18 (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
6058, 59bitr4i 267 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61 ne0i 4067 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
6260, 61sylbir 225 . . . . . . . . . . . . . . . 16 (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6362exlimiv 2009 . . . . . . . . . . . . . . 15 (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6456, 63sylbi 207 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65 df-fr 5208 . . . . . . . . . . . . . . 15 (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏))
6622imaex 7250 . . . . . . . . . . . . . . . 16 (𝑠 “ {𝑎}) ∈ V
67 sseq1 3773 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68 neeq1 3004 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
6967, 68anbi12d 608 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → ((𝑣𝐵𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70 raleq 3286 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7170rexeqbi1dv 3295 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7269, 71imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑠 “ {𝑎}) → (((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
7366, 72spcv 3448 . . . . . . . . . . . . . . 15 (∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7465, 73sylbi 207 . . . . . . . . . . . . . 14 (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7554, 64, 74syl2ani 586 . . . . . . . . . . . . 13 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76 1stdm 7363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → (1st𝑤) ∈ dom 𝑠)
77 breq1 4787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (1st𝑤) → (𝑐𝑅𝑎 ↔ (1st𝑤)𝑅𝑎))
7877notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (1st𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st𝑤)𝑅𝑎))
7978rspccv 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st𝑤) ∈ dom 𝑠 → ¬ (1st𝑤)𝑅𝑎))
8076, 79syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠𝑤𝑠) → ¬ (1st𝑤)𝑅𝑎))
8180expd 400 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎)))
8281impcom 394 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
8382adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
84 elrel 5362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
8584ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel 𝑠 → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
8685adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87 vex 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑢 ∈ V
8855, 87elimasn 5631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89 breq1 4787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = 𝑢 → (𝑑𝑆𝑏𝑢𝑆𝑏))
9089notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
9190rspccv 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
9288, 91syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
9392adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94 opeq1 4537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
9594eleq1d 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
9695imbi1d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9793, 96syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9897com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99 eleq1 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100 vex 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡 ∈ V
101100, 87op1std 7324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → (1st𝑤) = 𝑡)
102101eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎𝑡 = 𝑎))
103100, 87op2ndd 7325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd𝑤) = 𝑢)
104103breq1d 4794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd𝑤)𝑆𝑏𝑢𝑆𝑏))
105104notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106102, 105imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
10799, 106imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
10898, 107syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
109108exlimivv 2011 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
110109com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11186, 110mpdd 43 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
112111adantlr 686 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
11383, 112jcad 496 . . . . . . . . . . . . . . . . . . . . . 22 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
114113ralrimiv 3113 . . . . . . . . . . . . . . . . . . . . 21 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
115114ex 397 . . . . . . . . . . . . . . . . . . . 20 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11615, 115sylan 561 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
117 olc 848 . . . . . . . . . . . . . . . . . . . 20 ((¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
118117ralimi 3100 . . . . . . . . . . . . . . . . . . 19 (∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
119116, 118syl6 35 . . . . . . . . . . . . . . . . . 18 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))))
120 ianor 910 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
121 vex 3352 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
122 opex 5060 . . . . . . . . . . . . . . . . . . . . . 22 𝑎, 𝑏⟩ ∈ V
123 eleq1 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124123anbi1d 607 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → (1st𝑥) = (1st𝑤))
126125breq1d 4794 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → ((1st𝑥)𝑅(1st𝑦) ↔ (1st𝑤)𝑅(1st𝑦)))
127125eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((1st𝑥) = (1st𝑦) ↔ (1st𝑤) = (1st𝑦)))
128 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (2nd𝑥) = (2nd𝑤))
129128breq1d 4794 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((2nd𝑥)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆(2nd𝑦)))
130127, 129anbi12d 608 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))
131126, 130orbi12d 883 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)))))
132124, 131anbi12d 608 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))))
133 eleq1 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134133anbi2d 606 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
13555, 57op1std 7324 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → (1st𝑦) = 𝑎)
136135breq2d 4796 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤)𝑅(1st𝑦) ↔ (1st𝑤)𝑅𝑎))
137135eqeq2d 2780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤) = (1st𝑦) ↔ (1st𝑤) = 𝑎))
13855, 57op2ndd 7325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
139138breq2d 4796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑤)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆𝑏))
140137, 139anbi12d 608 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)) ↔ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
141136, 140orbi12d 883 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
142134, 141anbi12d 608 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = ⟨𝑎, 𝑏⟩ → (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))))
143 frxp.1 . . . . . . . . . . . . . . . . . . . . . 22 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))))}
144121, 122, 132, 142, 143brab 5131 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑇𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
145120, 144xchnxbir 322 . . . . . . . . . . . . . . . . . . . 20 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
146 ioran 912 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
147 ianor 910 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
148 pm4.62 835 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
149147, 148bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))
150149anbi2i 601 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
151146, 150bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
152151orbi2i 877 . . . . . . . . . . . . . . . . . . . 20 ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
153145, 152bitri 264 . . . . . . . . . . . . . . . . . . 19 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
154153ralbii 3128 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
155119, 154syl6ibr 242 . . . . . . . . . . . . . . . . 17 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
156155reximdv 3163 . . . . . . . . . . . . . . . 16 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
157156ex 397 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
158157com23 86 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
159158adantr 466 . . . . . . . . . . . . 13 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
16075, 159sylcom 30 . . . . . . . . . . . 12 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
161160impl 443 . . . . . . . . . . 11 (((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
162161expimpd 441 . . . . . . . . . 10 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
1631623adant3 1125 . . . . . . . . 9 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
164 resss 5563 . . . . . . . . . 10 (𝑠 ↾ {𝑎}) ⊆ 𝑠
165 df-rex 3066 . . . . . . . . . . . . 13 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
166 eqid 2770 . . . . . . . . . . . . . . . 16 𝑎, 𝑏⟩ = ⟨𝑎, 𝑏
167 eqeq1 2774 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168 breq2 4788 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧𝑤𝑇𝑎, 𝑏⟩))
169168notbid 307 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇𝑎, 𝑏⟩))
170169ralbidv 3134 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
171170anbi2d 606 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
172167, 171anbi12d 608 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))))
173122, 172spcev 3449 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
174166, 173mpan 662 . . . . . . . . . . . . . . 15 ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
17558, 174sylanb 562 . . . . . . . . . . . . . 14 ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
176175eximi 1909 . . . . . . . . . . . . 13 (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
177165, 176sylbi 207 . . . . . . . . . . . 12 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
178 excom 2197 . . . . . . . . . . . 12 (∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
179177, 178sylib 208 . . . . . . . . . . 11 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
180 df-rex 3066 . . . . . . . . . . . 12 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
18155elsnres 5577 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182181anbi1i 602 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
183 19.41v 2028 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
184 anass 459 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
185184exbii 1923 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
186182, 183, 1853bitr2i 288 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
187186exbii 1923 . . . . . . . . . . . 12 (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
188180, 187bitri 264 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
189179, 188sylibr 224 . . . . . . . . . 10 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧)
190 ssrexv 3814 . . . . . . . . . 10 ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
191164, 189, 190mpsyl 68 . . . . . . . . 9 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)
192163, 191syl6 35 . . . . . . . 8 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
193192expd 400 . . . . . . 7 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
194193rexlimdv 3177 . . . . . 6 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
1951943expib 1115 . . . . 5 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
196195adantl 467 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
19733, 196mpdd 43 . . 3 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
198197alrimiv 2006 . 2 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
199 df-fr 5208 . 2 (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
200198, 199sylibr 224 1 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826  w3a 1070  wal 1628   = wceq 1630  wex 1851  wcel 2144  wne 2942  wral 3060  wrex 3061  wss 3721  c0 4061  {csn 4314  cop 4320   class class class wbr 4784  {copab 4844   Fr wfr 5205   × cxp 5247  dom cdm 5249  ran crn 5250  cres 5251  cima 5252  Rel wrel 5254  cfv 6031  1st c1st 7312  2nd c2nd 7313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-int 4610  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-fr 5208  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fv 6039  df-1st 7314  df-2nd 7315
This theorem is referenced by:  wexp  7441
  Copyright terms: Public domain W3C validator