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

Theorem frxp 8058
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 4360 . . . . . . . . 9 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2 xpnz 6111 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
32biimpri 227 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
43simprd 496 . . . . . . . . 9 ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
51, 4syl 17 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6 dmxp 5884 . . . . . . . . . 10 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7 dmss 5858 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8 sseq2 3970 . . . . . . . . . . 11 (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠𝐴))
97, 8imbitrid 243 . . . . . . . . . 10 (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
106, 9syl 17 . . . . . . . . 9 (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
1110impcom 408 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠𝐴)
125, 11syldan 591 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠𝐴)
13 relxp 5651 . . . . . . . . . . 11 Rel (𝐴 × 𝐵)
14 relss 5737 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
1513, 14mpi 20 . . . . . . . . . 10 (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16 reldm0 5883 . . . . . . . . . 10 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1715, 16syl 17 . . . . . . . . 9 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1817necon3bid 2988 . . . . . . . 8 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
1918biimpa 477 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
2012, 19jca 512 . . . . . 6 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅))
21 df-fr 5588 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎))
22 vex 3449 . . . . . . . . 9 𝑠 ∈ V
2322dmex 7848 . . . . . . . 8 dom 𝑠 ∈ V
24 sseq1 3969 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣𝐴 ↔ dom 𝑠𝐴))
25 neeq1 3006 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
2624, 25anbi12d 631 . . . . . . . . 9 (𝑣 = dom 𝑠 → ((𝑣𝐴𝑣 ≠ ∅) ↔ (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅)))
27 raleq 3309 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (∀𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2827rexeqbi1dv 3308 . . . . . . . . 9 (𝑣 = dom 𝑠 → (∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2926, 28imbi12d 344 . . . . . . . 8 (𝑣 = dom 𝑠 → (((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
3023, 29spcv 3564 . . . . . . 7 (∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3121, 30sylbi 216 . . . . . 6 (𝑅 Fr 𝐴 → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3220, 31syl5 34 . . . . 5 (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3332adantr 481 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34 imassrn 6024 . . . . . . . . . . . . . . 15 (𝑠 “ {𝑎}) ⊆ ran 𝑠
35 xpeq0 6112 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
3635biimpri 227 . . . . . . . . . . . . . . . . . . 19 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
3736orcs 873 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38 sseq2 3970 . . . . . . . . . . . . . . . . . . 19 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39 ss0 4358 . . . . . . . . . . . . . . . . . . 19 (𝑠 ⊆ ∅ → 𝑠 = ∅)
4038, 39syl6bi 252 . . . . . . . . . . . . . . . . . 18 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
4137, 40syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42 rneq 5891 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → ran 𝑠 = ran ∅)
43 rn0 5881 . . . . . . . . . . . . . . . . . . 19 ran ∅ = ∅
44 0ss 4356 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝐵
4543, 44eqsstri 3978 . . . . . . . . . . . . . . . . . 18 ran ∅ ⊆ 𝐵
4642, 45eqsstrdi 3998 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → ran 𝑠𝐵)
4741, 46syl6 35 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
48 rnxp 6122 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49 rnss 5894 . . . . . . . . . . . . . . . . . 18 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50 sseq2 3970 . . . . . . . . . . . . . . . . . 18 (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠𝐵))
5149, 50imbitrid 243 . . . . . . . . . . . . . . . . 17 (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5248, 51syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5347, 52pm2.61ine 3028 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵)
5434, 53sstrid 3955 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55 vex 3449 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
5655eldm 5856 . . . . . . . . . . . . . . 15 (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑏 ∈ V
5855, 57elimasn 6041 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59 df-br 5106 . . . . . . . . . . . . . . . . . 18 (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
6058, 59bitr4i 277 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61 ne0i 4294 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
6260, 61sylbir 234 . . . . . . . . . . . . . . . 16 (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6362exlimiv 1933 . . . . . . . . . . . . . . 15 (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6456, 63sylbi 216 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65 df-fr 5588 . . . . . . . . . . . . . . 15 (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏))
6622imaex 7853 . . . . . . . . . . . . . . . 16 (𝑠 “ {𝑎}) ∈ V
67 sseq1 3969 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68 neeq1 3006 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
6967, 68anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → ((𝑣𝐵𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70 raleq 3309 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7170rexeqbi1dv 3308 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7269, 71imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑠 “ {𝑎}) → (((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
7366, 72spcv 3564 . . . . . . . . . . . . . . 15 (∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7465, 73sylbi 216 . . . . . . . . . . . . . 14 (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7554, 64, 74syl2ani 607 . . . . . . . . . . . . 13 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76 1stdm 7972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → (1st𝑤) ∈ dom 𝑠)
77 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (1st𝑤) → (𝑐𝑅𝑎 ↔ (1st𝑤)𝑅𝑎))
7877notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (1st𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st𝑤)𝑅𝑎))
7978rspccv 3578 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st𝑤) ∈ dom 𝑠 → ¬ (1st𝑤)𝑅𝑎))
8076, 79syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠𝑤𝑠) → ¬ (1st𝑤)𝑅𝑎))
8180expd 416 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎)))
8281impcom 408 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
8382adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
84 elrel 5754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
8584ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel 𝑠 → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
8685adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑢 ∈ V
8855, 87elimasn 6041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = 𝑢 → (𝑑𝑆𝑏𝑢𝑆𝑏))
9089notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
9190rspccv 3578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
9288, 91biimtrrid 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
9392adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94 opeq1 4830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
9594eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
9695imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9793, 96syl5ibr 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9897com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡 ∈ V
101100, 87op1std 7931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → (1st𝑤) = 𝑡)
102101eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎𝑡 = 𝑎))
103100, 87op2ndd 7932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd𝑤) = 𝑢)
104103breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd𝑤)𝑆𝑏𝑢𝑆𝑏))
105104notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106102, 105imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
10799, 106imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
10898, 107syl5ibr 245 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
109108exlimivv 1935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
110109com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11186, 110mpdd 43 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
112111adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
11383, 112jcad 513 . . . . . . . . . . . . . . . . . . . . . 22 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
114113ralrimiv 3142 . . . . . . . . . . . . . . . . . . . . 21 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
115114ex 413 . . . . . . . . . . . . . . . . . . . 20 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11615, 115sylan 580 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
117 olc 866 . . . . . . . . . . . . . . . . . . . 20 ((¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
118117ralimi 3086 . . . . . . . . . . . . . . . . . . 19 (∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
119116, 118syl6 35 . . . . . . . . . . . . . . . . . 18 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))))
120 ianor 980 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
121 vex 3449 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
122 opex 5421 . . . . . . . . . . . . . . . . . . . . . 22 𝑎, 𝑏⟩ ∈ V
123 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124123anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → (1st𝑥) = (1st𝑤))
126125breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → ((1st𝑥)𝑅(1st𝑦) ↔ (1st𝑤)𝑅(1st𝑦)))
127125eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((1st𝑥) = (1st𝑦) ↔ (1st𝑤) = (1st𝑦)))
128 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (2nd𝑥) = (2nd𝑤))
129128breq1d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((2nd𝑥)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆(2nd𝑦)))
130127, 129anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))
131126, 130orbi12d 917 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)))))
132124, 131anbi12d 631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))))
133 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134133anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
13555, 57op1std 7931 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → (1st𝑦) = 𝑎)
136135breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤)𝑅(1st𝑦) ↔ (1st𝑤)𝑅𝑎))
137135eqeq2d 2747 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤) = (1st𝑦) ↔ (1st𝑤) = 𝑎))
13855, 57op2ndd 7932 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
139138breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑤)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆𝑏))
140137, 139anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)) ↔ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
141136, 140orbi12d 917 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
142134, 141anbi12d 631 . . . . . . . . . . . . . . . . . . . . . 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 5500 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑇𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
145120, 144xchnxbir 332 . . . . . . . . . . . . . . . . . . . 20 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
146 ioran 982 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
147 ianor 980 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
148 pm4.62 854 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
149147, 148bitr4i 277 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))
150149anbi2i 623 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
151146, 150bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
152151orbi2i 911 . . . . . . . . . . . . . . . . . . . 20 ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
153145, 152bitri 274 . . . . . . . . . . . . . . . . . . 19 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
154153ralbii 3096 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
155119, 154syl6ibr 251 . . . . . . . . . . . . . . . . 17 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
156155reximdv 3167 . . . . . . . . . . . . . . . 16 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
157156ex 413 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
158157com23 86 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
159158adantr 481 . . . . . . . . . . . . 13 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
16075, 159sylcom 30 . . . . . . . . . . . 12 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
161160impl 456 . . . . . . . . . . 11 (((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
162161expimpd 454 . . . . . . . . . 10 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
1631623adant3 1132 . . . . . . . . 9 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
164 resss 5962 . . . . . . . . . 10 (𝑠 ↾ {𝑎}) ⊆ 𝑠
165 df-rex 3074 . . . . . . . . . . . . 13 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
166 eqid 2736 . . . . . . . . . . . . . . . 16 𝑎, 𝑏⟩ = ⟨𝑎, 𝑏
167 eqeq1 2740 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168 breq2 5109 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧𝑤𝑇𝑎, 𝑏⟩))
169168notbid 317 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇𝑎, 𝑏⟩))
170169ralbidv 3174 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
171170anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
172167, 171anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))))
173122, 172spcev 3565 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
174166, 173mpan 688 . . . . . . . . . . . . . . 15 ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
17558, 174sylanb 581 . . . . . . . . . . . . . 14 ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
176175eximi 1837 . . . . . . . . . . . . 13 (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
177165, 176sylbi 216 . . . . . . . . . . . 12 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
178 excom 2162 . . . . . . . . . . . 12 (∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
179177, 178sylib 217 . . . . . . . . . . 11 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
180 df-rex 3074 . . . . . . . . . . . 12 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
18155elsnres 5977 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182181anbi1i 624 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
183 19.41v 1953 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
184 anass 469 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
185184exbii 1850 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
186182, 183, 1853bitr2i 298 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
187186exbii 1850 . . . . . . . . . . . 12 (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
188180, 187bitri 274 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
189179, 188sylibr 233 . . . . . . . . . 10 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧)
190 ssrexv 4011 . . . . . . . . . 10 ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
191164, 189, 190mpsyl 68 . . . . . . . . 9 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)
192163, 191syl6 35 . . . . . . . 8 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
193192expd 416 . . . . . . 7 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
194193rexlimdv 3150 . . . . . 6 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
1951943expib 1122 . . . . 5 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
196195adantl 482 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
19733, 196mpdd 43 . . 3 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
198197alrimiv 1930 . 2 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
199 df-fr 5588 . 2 (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
200198, 199sylibr 233 1 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  wss 3910  c0 4282  {csn 4586  cop 4592   class class class wbr 5105  {copab 5167   Fr wfr 5585   × cxp 5631  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Rel wrel 5638  cfv 6496  1st c1st 7919  2nd c2nd 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-fr 5588  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922
This theorem is referenced by:  wexp  8062
  Copyright terms: Public domain W3C validator