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

Theorem frxp 7455
 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 4119 . . . . . . . . 9 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2 xpnz 5711 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
32biimpri 218 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
43simprd 482 . . . . . . . . 9 ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
51, 4syl 17 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6 dmxp 5499 . . . . . . . . . 10 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7 dmss 5478 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8 sseq2 3768 . . . . . . . . . . 11 (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠𝐴))
97, 8syl5ib 234 . . . . . . . . . 10 (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
106, 9syl 17 . . . . . . . . 9 (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
1110impcom 445 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠𝐴)
125, 11syldan 488 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠𝐴)
13 relxp 5283 . . . . . . . . . . 11 Rel (𝐴 × 𝐵)
14 relss 5363 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
1513, 14mpi 20 . . . . . . . . . 10 (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16 reldm0 5498 . . . . . . . . . 10 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1715, 16syl 17 . . . . . . . . 9 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1817necon3bid 2976 . . . . . . . 8 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
1918biimpa 502 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
2012, 19jca 555 . . . . . 6 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅))
21 df-fr 5225 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎))
22 vex 3343 . . . . . . . . 9 𝑠 ∈ V
2322dmex 7264 . . . . . . . 8 dom 𝑠 ∈ V
24 sseq1 3767 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣𝐴 ↔ dom 𝑠𝐴))
25 neeq1 2994 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
2624, 25anbi12d 749 . . . . . . . . 9 (𝑣 = dom 𝑠 → ((𝑣𝐴𝑣 ≠ ∅) ↔ (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅)))
27 raleq 3277 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (∀𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2827rexeqbi1dv 3286 . . . . . . . . 9 (𝑣 = dom 𝑠 → (∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2926, 28imbi12d 333 . . . . . . . 8 (𝑣 = dom 𝑠 → (((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
3023, 29spcv 3439 . . . . . . 7 (∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3121, 30sylbi 207 . . . . . 6 (𝑅 Fr 𝐴 → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3220, 31syl5 34 . . . . 5 (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3332adantr 472 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34 imassrn 5635 . . . . . . . . . . . . . . 15 (𝑠 “ {𝑎}) ⊆ ran 𝑠
35 xpeq0 5712 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
3635biimpri 218 . . . . . . . . . . . . . . . . . . 19 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
3736orcs 408 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38 sseq2 3768 . . . . . . . . . . . . . . . . . . 19 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39 ss0 4117 . . . . . . . . . . . . . . . . . . 19 (𝑠 ⊆ ∅ → 𝑠 = ∅)
4038, 39syl6bi 243 . . . . . . . . . . . . . . . . . 18 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
4137, 40syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42 rneq 5506 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → ran 𝑠 = ran ∅)
43 rn0 5532 . . . . . . . . . . . . . . . . . . 19 ran ∅ = ∅
44 0ss 4115 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝐵
4543, 44eqsstri 3776 . . . . . . . . . . . . . . . . . 18 ran ∅ ⊆ 𝐵
4642, 45syl6eqss 3796 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → ran 𝑠𝐵)
4741, 46syl6 35 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
48 rnxp 5722 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49 rnss 5509 . . . . . . . . . . . . . . . . . 18 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50 sseq2 3768 . . . . . . . . . . . . . . . . . 18 (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠𝐵))
5149, 50syl5ib 234 . . . . . . . . . . . . . . . . 17 (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5248, 51syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5347, 52pm2.61ine 3015 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵)
5434, 53syl5ss 3755 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55 vex 3343 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
5655eldm 5476 . . . . . . . . . . . . . . 15 (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57 vex 3343 . . . . . . . . . . . . . . . . . . 19 𝑏 ∈ V
5855, 57elimasn 5648 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59 df-br 4805 . . . . . . . . . . . . . . . . . 18 (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
6058, 59bitr4i 267 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61 ne0i 4064 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
6260, 61sylbir 225 . . . . . . . . . . . . . . . 16 (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6362exlimiv 2007 . . . . . . . . . . . . . . 15 (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6456, 63sylbi 207 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65 df-fr 5225 . . . . . . . . . . . . . . 15 (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏))
6622imaex 7269 . . . . . . . . . . . . . . . 16 (𝑠 “ {𝑎}) ∈ V
67 sseq1 3767 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68 neeq1 2994 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
6967, 68anbi12d 749 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → ((𝑣𝐵𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70 raleq 3277 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7170rexeqbi1dv 3286 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7269, 71imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑠 “ {𝑎}) → (((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
7366, 72spcv 3439 . . . . . . . . . . . . . . 15 (∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7465, 73sylbi 207 . . . . . . . . . . . . . 14 (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7554, 64, 74syl2ani 691 . . . . . . . . . . . . 13 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76 1stdm 7382 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → (1st𝑤) ∈ dom 𝑠)
77 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (1st𝑤) → (𝑐𝑅𝑎 ↔ (1st𝑤)𝑅𝑎))
7877notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (1st𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st𝑤)𝑅𝑎))
7978rspccv 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st𝑤) ∈ dom 𝑠 → ¬ (1st𝑤)𝑅𝑎))
8076, 79syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠𝑤𝑠) → ¬ (1st𝑤)𝑅𝑎))
8180expd 451 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎)))
8281impcom 445 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
8382adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
84 elrel 5379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
8584ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel 𝑠 → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
8685adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑢 ∈ V
8855, 87elimasn 5648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = 𝑢 → (𝑑𝑆𝑏𝑢𝑆𝑏))
9089notbid 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
9190rspccv 3446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
9288, 91syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
9392adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94 opeq1 4553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
9594eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
9695imbi1d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9793, 96syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9897com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡 ∈ V
101100, 87op1std 7343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → (1st𝑤) = 𝑡)
102101eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎𝑡 = 𝑎))
103100, 87op2ndd 7344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd𝑤) = 𝑢)
104103breq1d 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2009 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
110109com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11186, 110mpdd 43 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
112111adantlr 753 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
11383, 112jcad 556 . . . . . . . . . . . . . . . . . . . . . 22 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
114113ralrimiv 3103 . . . . . . . . . . . . . . . . . . . . 21 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
115114ex 449 . . . . . . . . . . . . . . . . . . . 20 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11615, 115sylan 489 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
117 olc 398 . . . . . . . . . . . . . . . . . . . 20 ((¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
118117ralimi 3090 . . . . . . . . . . . . . . . . . . 19 (∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
119116, 118syl6 35 . . . . . . . . . . . . . . . . . 18 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))))
120 ianor 510 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
121 vex 3343 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
122 opex 5081 . . . . . . . . . . . . . . . . . . . . . 22 𝑎, 𝑏⟩ ∈ V
123 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124123anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → (1st𝑥) = (1st𝑤))
126125breq1d 4814 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → ((1st𝑥)𝑅(1st𝑦) ↔ (1st𝑤)𝑅(1st𝑦)))
127125eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((1st𝑥) = (1st𝑦) ↔ (1st𝑤) = (1st𝑦)))
128 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (2nd𝑥) = (2nd𝑤))
129128breq1d 4814 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((2nd𝑥)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆(2nd𝑦)))
130127, 129anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))
131126, 130orbi12d 748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)))))
132124, 131anbi12d 749 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))))
133 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134133anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
13555, 57op1std 7343 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → (1st𝑦) = 𝑎)
136135breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤)𝑅(1st𝑦) ↔ (1st𝑤)𝑅𝑎))
137135eqeq2d 2770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤) = (1st𝑦) ↔ (1st𝑤) = 𝑎))
13855, 57op2ndd 7344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
139138breq2d 4816 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑤)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆𝑏))
140137, 139anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)) ↔ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
141136, 140orbi12d 748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
142134, 141anbi12d 749 . . . . . . . . . . . . . . . . . . . . . 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 5148 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑇𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
145120, 144xchnxbir 322 . . . . . . . . . . . . . . . . . . . 20 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
146 ioran 512 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
147 ianor 510 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
148 pm4.62 434 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
149147, 148bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))
150149anbi2i 732 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
151146, 150bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
152151orbi2i 542 . . . . . . . . . . . . . . . . . . . 20 ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
153145, 152bitri 264 . . . . . . . . . . . . . . . . . . 19 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
154153ralbii 3118 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
155119, 154syl6ibr 242 . . . . . . . . . . . . . . . . 17 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
156155reximdv 3154 . . . . . . . . . . . . . . . 16 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
157156ex 449 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
158157com23 86 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
159158adantr 472 . . . . . . . . . . . . 13 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
16075, 159sylcom 30 . . . . . . . . . . . 12 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
161160impl 651 . . . . . . . . . . 11 (((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
162161expimpd 630 . . . . . . . . . 10 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
1631623adant3 1127 . . . . . . . . 9 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
164 resss 5580 . . . . . . . . . 10 (𝑠 ↾ {𝑎}) ⊆ 𝑠
165 df-rex 3056 . . . . . . . . . . . . 13 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
166 eqid 2760 . . . . . . . . . . . . . . . 16 𝑎, 𝑏⟩ = ⟨𝑎, 𝑏
167 eqeq1 2764 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168 breq2 4808 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧𝑤𝑇𝑎, 𝑏⟩))
169168notbid 307 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇𝑎, 𝑏⟩))
170169ralbidv 3124 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
171170anbi2d 742 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
172167, 171anbi12d 749 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))))
173122, 172spcev 3440 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
174166, 173mpan 708 . . . . . . . . . . . . . . 15 ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
17558, 174sylanb 490 . . . . . . . . . . . . . 14 ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
176175eximi 1911 . . . . . . . . . . . . 13 (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
177165, 176sylbi 207 . . . . . . . . . . . 12 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
178 excom 2191 . . . . . . . . . . . 12 (∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
179177, 178sylib 208 . . . . . . . . . . 11 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
180 df-rex 3056 . . . . . . . . . . . 12 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
18155elsnres 5594 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182181anbi1i 733 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
183 19.41v 2026 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
184 anass 684 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
185184exbii 1923 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
186182, 183, 1853bitr2i 288 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
187186exbii 1923 . . . . . . . . . . . 12 (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
188180, 187bitri 264 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
189179, 188sylibr 224 . . . . . . . . . 10 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧)
190 ssrexv 3808 . . . . . . . . . 10 ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
191164, 189, 190mpsyl 68 . . . . . . . . 9 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)
192163, 191syl6 35 . . . . . . . 8 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
193192expd 451 . . . . . . 7 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
194193rexlimdv 3168 . . . . . 6 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
1951943expib 1117 . . . . 5 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
196195adantl 473 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
19733, 196mpdd 43 . . 3 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
198197alrimiv 2004 . 2 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
199 df-fr 5225 . 2 (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
200198, 199sylibr 224 1 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1072  ∀wal 1630   = wceq 1632  ∃wex 1853   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051   ⊆ wss 3715  ∅c0 4058  {csn 4321  ⟨cop 4327   class class class wbr 4804  {copab 4864   Fr wfr 5222   × cxp 5264  dom cdm 5266  ran crn 5267   ↾ cres 5268   “ cima 5269  Rel wrel 5271  ‘cfv 6049  1st c1st 7331  2nd c2nd 7332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-int 4628  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-fr 5225  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fv 6057  df-1st 7333  df-2nd 7334 This theorem is referenced by:  wexp  7459
 Copyright terms: Public domain W3C validator