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

Theorem frxp 7521
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 4174 . . . . . . . . 9 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2 xpnz 5764 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
32biimpri 219 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
43simprd 485 . . . . . . . . 9 ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
51, 4syl 17 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6 dmxp 5545 . . . . . . . . . 10 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7 dmss 5524 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8 sseq2 3824 . . . . . . . . . . 11 (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠𝐴))
97, 8syl5ib 235 . . . . . . . . . 10 (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
106, 9syl 17 . . . . . . . . 9 (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
1110impcom 396 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠𝐴)
125, 11syldan 581 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠𝐴)
13 relxp 5328 . . . . . . . . . . 11 Rel (𝐴 × 𝐵)
14 relss 5408 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
1513, 14mpi 20 . . . . . . . . . 10 (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16 reldm0 5544 . . . . . . . . . 10 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1715, 16syl 17 . . . . . . . . 9 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1817necon3bid 3022 . . . . . . . 8 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
1918biimpa 464 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
2012, 19jca 503 . . . . . 6 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅))
21 df-fr 5270 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎))
22 vex 3394 . . . . . . . . 9 𝑠 ∈ V
2322dmex 7329 . . . . . . . 8 dom 𝑠 ∈ V
24 sseq1 3823 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣𝐴 ↔ dom 𝑠𝐴))
25 neeq1 3040 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
2624, 25anbi12d 618 . . . . . . . . 9 (𝑣 = dom 𝑠 → ((𝑣𝐴𝑣 ≠ ∅) ↔ (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅)))
27 raleq 3327 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (∀𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2827rexeqbi1dv 3336 . . . . . . . . 9 (𝑣 = dom 𝑠 → (∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2926, 28imbi12d 335 . . . . . . . 8 (𝑣 = dom 𝑠 → (((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
3023, 29spcv 3492 . . . . . . 7 (∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3121, 30sylbi 208 . . . . . 6 (𝑅 Fr 𝐴 → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3220, 31syl5 34 . . . . 5 (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3332adantr 468 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34 imassrn 5687 . . . . . . . . . . . . . . 15 (𝑠 “ {𝑎}) ⊆ ran 𝑠
35 xpeq0 5765 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
3635biimpri 219 . . . . . . . . . . . . . . . . . . 19 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
3736orcs 893 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38 sseq2 3824 . . . . . . . . . . . . . . . . . . 19 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39 ss0 4172 . . . . . . . . . . . . . . . . . . 19 (𝑠 ⊆ ∅ → 𝑠 = ∅)
4038, 39syl6bi 244 . . . . . . . . . . . . . . . . . 18 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
4137, 40syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42 rneq 5552 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → ran 𝑠 = ran ∅)
43 rn0 5578 . . . . . . . . . . . . . . . . . . 19 ran ∅ = ∅
44 0ss 4170 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝐵
4543, 44eqsstri 3832 . . . . . . . . . . . . . . . . . 18 ran ∅ ⊆ 𝐵
4642, 45syl6eqss 3852 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → ran 𝑠𝐵)
4741, 46syl6 35 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
48 rnxp 5775 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49 rnss 5555 . . . . . . . . . . . . . . . . . 18 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50 sseq2 3824 . . . . . . . . . . . . . . . . . 18 (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠𝐵))
5149, 50syl5ib 235 . . . . . . . . . . . . . . . . 17 (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5248, 51syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5347, 52pm2.61ine 3061 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵)
5434, 53syl5ss 3809 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55 vex 3394 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
5655eldm 5522 . . . . . . . . . . . . . . 15 (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57 vex 3394 . . . . . . . . . . . . . . . . . . 19 𝑏 ∈ V
5855, 57elimasn 5700 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59 df-br 4845 . . . . . . . . . . . . . . . . . 18 (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
6058, 59bitr4i 269 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61 ne0i 4122 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
6260, 61sylbir 226 . . . . . . . . . . . . . . . 16 (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6362exlimiv 2021 . . . . . . . . . . . . . . 15 (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6456, 63sylbi 208 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65 df-fr 5270 . . . . . . . . . . . . . . 15 (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏))
6622imaex 7334 . . . . . . . . . . . . . . . 16 (𝑠 “ {𝑎}) ∈ V
67 sseq1 3823 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68 neeq1 3040 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
6967, 68anbi12d 618 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → ((𝑣𝐵𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70 raleq 3327 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7170rexeqbi1dv 3336 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7269, 71imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑠 “ {𝑎}) → (((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
7366, 72spcv 3492 . . . . . . . . . . . . . . 15 (∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7465, 73sylbi 208 . . . . . . . . . . . . . 14 (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7554, 64, 74syl2ani 596 . . . . . . . . . . . . 13 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76 1stdm 7447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → (1st𝑤) ∈ dom 𝑠)
77 breq1 4847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (1st𝑤) → (𝑐𝑅𝑎 ↔ (1st𝑤)𝑅𝑎))
7877notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (1st𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st𝑤)𝑅𝑎))
7978rspccv 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st𝑤) ∈ dom 𝑠 → ¬ (1st𝑤)𝑅𝑎))
8076, 79syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠𝑤𝑠) → ¬ (1st𝑤)𝑅𝑎))
8180expd 402 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎)))
8281impcom 396 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
8382adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
84 elrel 5424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
8584ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel 𝑠 → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
8685adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87 vex 3394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑢 ∈ V
8855, 87elimasn 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89 breq1 4847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = 𝑢 → (𝑑𝑆𝑏𝑢𝑆𝑏))
9089notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
9190rspccv 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
9288, 91syl5bir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
9392adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94 opeq1 4595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
9594eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
9695imbi1d 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9793, 96syl5ibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9897com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100 vex 3394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡 ∈ V
101100, 87op1std 7408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → (1st𝑤) = 𝑡)
102101eqeq1d 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎𝑡 = 𝑎))
103100, 87op2ndd 7409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd𝑤) = 𝑢)
104103breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd𝑤)𝑆𝑏𝑢𝑆𝑏))
105104notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106102, 105imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
10799, 106imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
10898, 107syl5ibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
109108exlimivv 2023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
110109com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11186, 110mpdd 43 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
112111adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
11383, 112jcad 504 . . . . . . . . . . . . . . . . . . . . . 22 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
114113ralrimiv 3153 . . . . . . . . . . . . . . . . . . . . 21 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
115114ex 399 . . . . . . . . . . . . . . . . . . . 20 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11615, 115sylan 571 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
117 olc 886 . . . . . . . . . . . . . . . . . . . 20 ((¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
118117ralimi 3140 . . . . . . . . . . . . . . . . . . 19 (∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
119116, 118syl6 35 . . . . . . . . . . . . . . . . . 18 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))))
120 ianor 995 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
121 vex 3394 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
122 opex 5122 . . . . . . . . . . . . . . . . . . . . . 22 𝑎, 𝑏⟩ ∈ V
123 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124123anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → (1st𝑥) = (1st𝑤))
126125breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → ((1st𝑥)𝑅(1st𝑦) ↔ (1st𝑤)𝑅(1st𝑦)))
127125eqeq1d 2808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((1st𝑥) = (1st𝑦) ↔ (1st𝑤) = (1st𝑦)))
128 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (2nd𝑥) = (2nd𝑤))
129128breq1d 4854 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((2nd𝑥)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆(2nd𝑦)))
130127, 129anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))
131126, 130orbi12d 933 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)))))
132124, 131anbi12d 618 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))))
133 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134133anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
13555, 57op1std 7408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → (1st𝑦) = 𝑎)
136135breq2d 4856 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤)𝑅(1st𝑦) ↔ (1st𝑤)𝑅𝑎))
137135eqeq2d 2816 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤) = (1st𝑦) ↔ (1st𝑤) = 𝑎))
13855, 57op2ndd 7409 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
139138breq2d 4856 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑤)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆𝑏))
140137, 139anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)) ↔ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
141136, 140orbi12d 933 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
142134, 141anbi12d 618 . . . . . . . . . . . . . . . . . . . . . 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 5193 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑇𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
145120, 144xchnxbir 324 . . . . . . . . . . . . . . . . . . . 20 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
146 ioran 997 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
147 ianor 995 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
148 pm4.62 874 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
149147, 148bitr4i 269 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))
150149anbi2i 611 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
151146, 150bitri 266 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
152151orbi2i 927 . . . . . . . . . . . . . . . . . . . 20 ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
153145, 152bitri 266 . . . . . . . . . . . . . . . . . . 19 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
154153ralbii 3168 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
155119, 154syl6ibr 243 . . . . . . . . . . . . . . . . 17 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
156155reximdv 3203 . . . . . . . . . . . . . . . 16 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
157156ex 399 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
158157com23 86 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
159158adantr 468 . . . . . . . . . . . . 13 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
16075, 159sylcom 30 . . . . . . . . . . . 12 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
161160impl 445 . . . . . . . . . . 11 (((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
162161expimpd 443 . . . . . . . . . 10 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
1631623adant3 1155 . . . . . . . . 9 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
164 resss 5625 . . . . . . . . . 10 (𝑠 ↾ {𝑎}) ⊆ 𝑠
165 df-rex 3102 . . . . . . . . . . . . 13 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
166 eqid 2806 . . . . . . . . . . . . . . . 16 𝑎, 𝑏⟩ = ⟨𝑎, 𝑏
167 eqeq1 2810 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168 breq2 4848 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧𝑤𝑇𝑎, 𝑏⟩))
169168notbid 309 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇𝑎, 𝑏⟩))
170169ralbidv 3174 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
171170anbi2d 616 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
172167, 171anbi12d 618 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))))
173122, 172spcev 3493 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
174166, 173mpan 673 . . . . . . . . . . . . . . 15 ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
17558, 174sylanb 572 . . . . . . . . . . . . . 14 ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
176175eximi 1919 . . . . . . . . . . . . 13 (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
177165, 176sylbi 208 . . . . . . . . . . . 12 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
178 excom 2209 . . . . . . . . . . . 12 (∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
179177, 178sylib 209 . . . . . . . . . . 11 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
180 df-rex 3102 . . . . . . . . . . . 12 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
18155elsnres 5640 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182181anbi1i 612 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
183 19.41v 2040 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
184 anass 456 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
185184exbii 1933 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
186182, 183, 1853bitr2i 290 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
187186exbii 1933 . . . . . . . . . . . 12 (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
188180, 187bitri 266 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
189179, 188sylibr 225 . . . . . . . . . 10 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧)
190 ssrexv 3864 . . . . . . . . . 10 ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
191164, 189, 190mpsyl 68 . . . . . . . . 9 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)
192163, 191syl6 35 . . . . . . . 8 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
193192expd 402 . . . . . . 7 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
194193rexlimdv 3218 . . . . . 6 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
1951943expib 1145 . . . . 5 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
196195adantl 469 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
19733, 196mpdd 43 . . 3 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
198197alrimiv 2018 . 2 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
199 df-fr 5270 . 2 (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
200198, 199sylibr 225 1 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100  wal 1635   = wceq 1637  wex 1859  wcel 2156  wne 2978  wral 3096  wrex 3097  wss 3769  c0 4116  {csn 4370  cop 4376   class class class wbr 4844  {copab 4906   Fr wfr 5267   × cxp 5309  dom cdm 5311  ran crn 5312  cres 5313  cima 5314  Rel wrel 5316  cfv 6101  1st c1st 7396  2nd c2nd 7397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-int 4670  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-fr 5270  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fv 6109  df-1st 7398  df-2nd 7399
This theorem is referenced by:  wexp  7525
  Copyright terms: Public domain W3C validator