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

Theorem frxp 7232
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 3948 . . . . . . . . 9 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝐴 × 𝐵) ≠ ∅)
2 xpnz 5512 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
32biimpri 218 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅))
43simprd 479 . . . . . . . . 9 ((𝐴 × 𝐵) ≠ ∅ → 𝐵 ≠ ∅)
51, 4syl 17 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → 𝐵 ≠ ∅)
6 dmxp 5304 . . . . . . . . . 10 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
7 dmss 5283 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠 ⊆ dom (𝐴 × 𝐵))
8 sseq2 3606 . . . . . . . . . . 11 (dom (𝐴 × 𝐵) = 𝐴 → (dom 𝑠 ⊆ dom (𝐴 × 𝐵) ↔ dom 𝑠𝐴))
97, 8syl5ib 234 . . . . . . . . . 10 (dom (𝐴 × 𝐵) = 𝐴 → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
106, 9syl 17 . . . . . . . . 9 (𝐵 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → dom 𝑠𝐴))
1110impcom 446 . . . . . . . 8 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝐵 ≠ ∅) → dom 𝑠𝐴)
125, 11syldan 487 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠𝐴)
13 relxp 5188 . . . . . . . . . . 11 Rel (𝐴 × 𝐵)
14 relss 5167 . . . . . . . . . . 11 (𝑠 ⊆ (𝐴 × 𝐵) → (Rel (𝐴 × 𝐵) → Rel 𝑠))
1513, 14mpi 20 . . . . . . . . . 10 (𝑠 ⊆ (𝐴 × 𝐵) → Rel 𝑠)
16 reldm0 5303 . . . . . . . . . 10 (Rel 𝑠 → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1715, 16syl 17 . . . . . . . . 9 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 = ∅ ↔ dom 𝑠 = ∅))
1817necon3bid 2834 . . . . . . . 8 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
1918biimpa 501 . . . . . . 7 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → dom 𝑠 ≠ ∅)
2012, 19jca 554 . . . . . 6 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅))
21 df-fr 5033 . . . . . . 7 (𝑅 Fr 𝐴 ↔ ∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎))
22 vex 3189 . . . . . . . . 9 𝑠 ∈ V
2322dmex 7046 . . . . . . . 8 dom 𝑠 ∈ V
24 sseq1 3605 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣𝐴 ↔ dom 𝑠𝐴))
25 neeq1 2852 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (𝑣 ≠ ∅ ↔ dom 𝑠 ≠ ∅))
2624, 25anbi12d 746 . . . . . . . . 9 (𝑣 = dom 𝑠 → ((𝑣𝐴𝑣 ≠ ∅) ↔ (dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅)))
27 raleq 3127 . . . . . . . . . 10 (𝑣 = dom 𝑠 → (∀𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2827rexeqbi1dv 3136 . . . . . . . . 9 (𝑣 = dom 𝑠 → (∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎 ↔ ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
2926, 28imbi12d 334 . . . . . . . 8 (𝑣 = dom 𝑠 → (((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) ↔ ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎)))
3023, 29spcv 3285 . . . . . . 7 (∀𝑣((𝑣𝐴𝑣 ≠ ∅) → ∃𝑎𝑣𝑐𝑣 ¬ 𝑐𝑅𝑎) → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3121, 30sylbi 207 . . . . . 6 (𝑅 Fr 𝐴 → ((dom 𝑠𝐴 ∧ dom 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3220, 31syl5 34 . . . . 5 (𝑅 Fr 𝐴 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
3332adantr 481 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎))
34 imassrn 5436 . . . . . . . . . . . . . . 15 (𝑠 “ {𝑎}) ⊆ ran 𝑠
35 xpeq0 5513 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
3635biimpri 218 . . . . . . . . . . . . . . . . . . 19 ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 × 𝐵) = ∅)
3736orcs 409 . . . . . . . . . . . . . . . . . 18 (𝐴 = ∅ → (𝐴 × 𝐵) = ∅)
38 sseq2 3606 . . . . . . . . . . . . . . . . . . 19 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) ↔ 𝑠 ⊆ ∅))
39 ss0 3946 . . . . . . . . . . . . . . . . . . 19 (𝑠 ⊆ ∅ → 𝑠 = ∅)
4038, 39syl6bi 243 . . . . . . . . . . . . . . . . . 18 ((𝐴 × 𝐵) = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
4137, 40syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → 𝑠 = ∅))
42 rneq 5311 . . . . . . . . . . . . . . . . . 18 (𝑠 = ∅ → ran 𝑠 = ran ∅)
43 rn0 5337 . . . . . . . . . . . . . . . . . . 19 ran ∅ = ∅
44 0ss 3944 . . . . . . . . . . . . . . . . . . 19 ∅ ⊆ 𝐵
4543, 44eqsstri 3614 . . . . . . . . . . . . . . . . . 18 ran ∅ ⊆ 𝐵
4642, 45syl6eqss 3634 . . . . . . . . . . . . . . . . 17 (𝑠 = ∅ → ran 𝑠𝐵)
4741, 46syl6 35 . . . . . . . . . . . . . . . 16 (𝐴 = ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
48 rnxp 5523 . . . . . . . . . . . . . . . . 17 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
49 rnss 5314 . . . . . . . . . . . . . . . . . 18 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠 ⊆ ran (𝐴 × 𝐵))
50 sseq2 3606 . . . . . . . . . . . . . . . . . 18 (ran (𝐴 × 𝐵) = 𝐵 → (ran 𝑠 ⊆ ran (𝐴 × 𝐵) ↔ ran 𝑠𝐵))
5149, 50syl5ib 234 . . . . . . . . . . . . . . . . 17 (ran (𝐴 × 𝐵) = 𝐵 → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5248, 51syl 17 . . . . . . . . . . . . . . . 16 (𝐴 ≠ ∅ → (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵))
5347, 52pm2.61ine 2873 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → ran 𝑠𝐵)
5434, 53syl5ss 3594 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (𝑠 “ {𝑎}) ⊆ 𝐵)
55 vex 3189 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
5655eldm 5281 . . . . . . . . . . . . . . 15 (𝑎 ∈ dom 𝑠 ↔ ∃𝑏 𝑎𝑠𝑏)
57 vex 3189 . . . . . . . . . . . . . . . . . . 19 𝑏 ∈ V
5855, 57elimasn 5449 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
59 df-br 4614 . . . . . . . . . . . . . . . . . 18 (𝑎𝑠𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝑠)
6058, 59bitr4i 267 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) ↔ 𝑎𝑠𝑏)
61 ne0i 3897 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑠 “ {𝑎}) → (𝑠 “ {𝑎}) ≠ ∅)
6260, 61sylbir 225 . . . . . . . . . . . . . . . 16 (𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6362exlimiv 1855 . . . . . . . . . . . . . . 15 (∃𝑏 𝑎𝑠𝑏 → (𝑠 “ {𝑎}) ≠ ∅)
6456, 63sylbi 207 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑠 → (𝑠 “ {𝑎}) ≠ ∅)
65 df-fr 5033 . . . . . . . . . . . . . . 15 (𝑆 Fr 𝐵 ↔ ∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏))
6622imaex 7051 . . . . . . . . . . . . . . . 16 (𝑠 “ {𝑎}) ∈ V
67 sseq1 3605 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣𝐵 ↔ (𝑠 “ {𝑎}) ⊆ 𝐵))
68 neeq1 2852 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (𝑣 ≠ ∅ ↔ (𝑠 “ {𝑎}) ≠ ∅))
6967, 68anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → ((𝑣𝐵𝑣 ≠ ∅) ↔ ((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅)))
70 raleq 3127 . . . . . . . . . . . . . . . . . 18 (𝑣 = (𝑠 “ {𝑎}) → (∀𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7170rexeqbi1dv 3136 . . . . . . . . . . . . . . . . 17 (𝑣 = (𝑠 “ {𝑎}) → (∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏 ↔ ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7269, 71imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑣 = (𝑠 “ {𝑎}) → (((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) ↔ (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏)))
7366, 72spcv 3285 . . . . . . . . . . . . . . 15 (∀𝑣((𝑣𝐵𝑣 ≠ ∅) → ∃𝑏𝑣𝑑𝑣 ¬ 𝑑𝑆𝑏) → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7465, 73sylbi 207 . . . . . . . . . . . . . 14 (𝑆 Fr 𝐵 → (((𝑠 “ {𝑎}) ⊆ 𝐵 ∧ (𝑠 “ {𝑎}) ≠ ∅) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
7554, 64, 74syl2ani 687 . . . . . . . . . . . . 13 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏))
76 1stdm 7160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → (1st𝑤) ∈ dom 𝑠)
77 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = (1st𝑤) → (𝑐𝑅𝑎 ↔ (1st𝑤)𝑅𝑎))
7877notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = (1st𝑤) → (¬ 𝑐𝑅𝑎 ↔ ¬ (1st𝑤)𝑅𝑎))
7978rspccv 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((1st𝑤) ∈ dom 𝑠 → ¬ (1st𝑤)𝑅𝑎))
8076, 79syl5 34 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ((Rel 𝑠𝑤𝑠) → ¬ (1st𝑤)𝑅𝑎))
8180expd 452 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (Rel 𝑠 → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎)))
8281impcom 446 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
8382adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ¬ (1st𝑤)𝑅𝑎))
84 elrel 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel 𝑠𝑤𝑠) → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩)
8584ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Rel 𝑠 → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
8685adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩))
87 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑢 ∈ V
8855, 87elimasn 5449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ (𝑠 “ {𝑎}) ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠)
89 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑑 = 𝑢 → (𝑑𝑆𝑏𝑢𝑆𝑏))
9089notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 = 𝑢 → (¬ 𝑑𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
9190rspccv 3292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (𝑢 ∈ (𝑠 “ {𝑎}) → ¬ 𝑢𝑆𝑏))
9288, 91syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
9392adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏))
94 opeq1 4370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 = 𝑎 → ⟨𝑡, 𝑢⟩ = ⟨𝑎, 𝑢⟩)
9594eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑡 = 𝑎 → (⟨𝑡, 𝑢⟩ ∈ 𝑠 ↔ ⟨𝑎, 𝑢⟩ ∈ 𝑠))
9695imbi1d 331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 = 𝑎 → ((⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏) ↔ (⟨𝑎, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9793, 96syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑡 = 𝑎 → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → ¬ 𝑢𝑆𝑏)))
9897com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
99 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (𝑤𝑠 ↔ ⟨𝑡, 𝑢⟩ ∈ 𝑠))
100 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡 ∈ V
101100, 87op1std 7123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → (1st𝑤) = 𝑡)
102101eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎𝑡 = 𝑎))
103100, 87op2ndd 7124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑤 = ⟨𝑡, 𝑢⟩ → (2nd𝑤) = 𝑢)
104103breq1d 4623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤 = ⟨𝑡, 𝑢⟩ → ((2nd𝑤)𝑆𝑏𝑢𝑆𝑏))
105104notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤 = ⟨𝑡, 𝑢⟩ → (¬ (2nd𝑤)𝑆𝑏 ↔ ¬ 𝑢𝑆𝑏))
106102, 105imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = ⟨𝑡, 𝑢⟩ → (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏)))
10799, 106imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = ⟨𝑡, 𝑢⟩ → ((𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) ↔ (⟨𝑡, 𝑢⟩ ∈ 𝑠 → (𝑡 = 𝑎 → ¬ 𝑢𝑆𝑏))))
10898, 107syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
109108exlimivv 1857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
110109com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (∃𝑡𝑢 𝑤 = ⟨𝑡, 𝑢⟩ → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11186, 110mpdd 43 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Rel 𝑠 ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
112111adantlr 750 . . . . . . . . . . . . . . . . . . . . . . 23 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
11383, 112jcad 555 . . . . . . . . . . . . . . . . . . . . . 22 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → (𝑤𝑠 → (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
114113ralrimiv 2959 . . . . . . . . . . . . . . . . . . . . 21 (((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) ∧ ∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏) → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
115114ex 450 . . . . . . . . . . . . . . . . . . . 20 ((Rel 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
11615, 115sylan 488 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
117 olc 399 . . . . . . . . . . . . . . . . . . . 20 ((¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
118117ralimi 2947 . . . . . . . . . . . . . . . . . . 19 (∀𝑤𝑠 (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)) → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
119116, 118syl6 35 . . . . . . . . . . . . . . . . . 18 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))))
120 ianor 509 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
121 vex 3189 . . . . . . . . . . . . . . . . . . . . . 22 𝑤 ∈ V
122 opex 4893 . . . . . . . . . . . . . . . . . . . . . 22 𝑎, 𝑏⟩ ∈ V
123 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (𝑥 ∈ (𝐴 × 𝐵) ↔ 𝑤 ∈ (𝐴 × 𝐵)))
124123anbi1d 740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵))))
125 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → (1st𝑥) = (1st𝑤))
126125breq1d 4623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → ((1st𝑥)𝑅(1st𝑦) ↔ (1st𝑤)𝑅(1st𝑦)))
127125eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((1st𝑥) = (1st𝑦) ↔ (1st𝑤) = (1st𝑦)))
128 fveq2 6148 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (2nd𝑥) = (2nd𝑤))
129128breq1d 4623 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ((2nd𝑥)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆(2nd𝑦)))
130127, 129anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑤 → (((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)) ↔ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))
131126, 130orbi12d 745 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑤 → (((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)))))
132124, 131anbi12d 746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑤 → (((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑥)𝑅(1st𝑦) ∨ ((1st𝑥) = (1st𝑦) ∧ (2nd𝑥)𝑆(2nd𝑦)))) ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))))))
133 eleq1 2686 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ (𝐴 × 𝐵) ↔ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)))
134133anbi2d 739 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ↔ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵))))
13555, 57op1std 7123 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → (1st𝑦) = 𝑎)
136135breq2d 4625 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤)𝑅(1st𝑦) ↔ (1st𝑤)𝑅𝑎))
137135eqeq2d 2631 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((1st𝑤) = (1st𝑦) ↔ (1st𝑤) = 𝑎))
13855, 57op2ndd 7124 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = ⟨𝑎, 𝑏⟩ → (2nd𝑦) = 𝑏)
139138breq2d 4625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = ⟨𝑎, 𝑏⟩ → ((2nd𝑤)𝑆(2nd𝑦) ↔ (2nd𝑤)𝑆𝑏))
140137, 139anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦)) ↔ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
141136, 140orbi12d 745 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = ⟨𝑎, 𝑏⟩ → (((1st𝑤)𝑅(1st𝑦) ∨ ((1st𝑤) = (1st𝑦) ∧ (2nd𝑤)𝑆(2nd𝑦))) ↔ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
142134, 141anbi12d 746 . . . . . . . . . . . . . . . . . . . . . 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 4958 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑇𝑎, 𝑏⟩ ↔ ((𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∧ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
145120, 144xchnxbir 323 . . . . . . . . . . . . . . . . . . . 20 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))))
146 ioran 511 . . . . . . . . . . . . . . . . . . . . . 22 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)))
147 ianor 509 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
148 pm4.62 435 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏) ↔ (¬ (1st𝑤) = 𝑎 ∨ ¬ (2nd𝑤)𝑆𝑏))
149147, 148bitr4i 267 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏) ↔ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))
150149anbi2i 729 . . . . . . . . . . . . . . . . . . . . . 22 ((¬ (1st𝑤)𝑅𝑎 ∧ ¬ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
151146, 150bitri 264 . . . . . . . . . . . . . . . . . . . . 21 (¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏)) ↔ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏)))
152151orbi2i 541 . . . . . . . . . . . . . . . . . . . 20 ((¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ ¬ ((1st𝑤)𝑅𝑎 ∨ ((1st𝑤) = 𝑎 ∧ (2nd𝑤)𝑆𝑏))) ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
153145, 152bitri 264 . . . . . . . . . . . . . . . . . . 19 𝑤𝑇𝑎, 𝑏⟩ ↔ (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
154153ralbii 2974 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∀𝑤𝑠 (¬ (𝑤 ∈ (𝐴 × 𝐵) ∧ ⟨𝑎, 𝑏⟩ ∈ (𝐴 × 𝐵)) ∨ (¬ (1st𝑤)𝑅𝑎 ∧ ((1st𝑤) = 𝑎 → ¬ (2nd𝑤)𝑆𝑏))))
155119, 154syl6ibr 242 . . . . . . . . . . . . . . . . 17 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
156155reximdv 3010 . . . . . . . . . . . . . . . 16 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
157156ex 450 . . . . . . . . . . . . . . 15 (𝑠 ⊆ (𝐴 × 𝐵) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
158157com23 86 . . . . . . . . . . . . . 14 (𝑠 ⊆ (𝐴 × 𝐵) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
159158adantr 481 . . . . . . . . . . . . 13 ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑑 ∈ (𝑠 “ {𝑎}) ¬ 𝑑𝑆𝑏 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
16075, 159sylcom 30 . . . . . . . . . . . 12 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
161160impl 649 . . . . . . . . . . 11 (((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) ∧ 𝑎 ∈ dom 𝑠) → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
162161expimpd 628 . . . . . . . . . 10 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵)) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
1631623adant3 1079 . . . . . . . . 9 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
164 resss 5381 . . . . . . . . . 10 (𝑠 ↾ {𝑎}) ⊆ 𝑠
165 df-rex 2913 . . . . . . . . . . . . 13 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ ↔ ∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
166 eqid 2621 . . . . . . . . . . . . . . . 16 𝑎, 𝑏⟩ = ⟨𝑎, 𝑏
167 eqeq1 2625 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩))
168 breq2 4617 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑤𝑇𝑧𝑤𝑇𝑎, 𝑏⟩))
169168notbid 308 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = ⟨𝑎, 𝑏⟩ → (¬ 𝑤𝑇𝑧 ↔ ¬ 𝑤𝑇𝑎, 𝑏⟩))
170169ralbidv 2980 . . . . . . . . . . . . . . . . . . 19 (𝑧 = ⟨𝑎, 𝑏⟩ → (∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))
171170anbi2d 739 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑎, 𝑏⟩ → ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)))
172167, 171anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑎, 𝑏⟩ → ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ (⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩))))
173122, 172spcev 3286 . . . . . . . . . . . . . . . 16 ((⟨𝑎, 𝑏⟩ = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩)) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
174166, 173mpan 705 . . . . . . . . . . . . . . 15 ((⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
17558, 174sylanb 489 . . . . . . . . . . . . . 14 ((𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
176175eximi 1759 . . . . . . . . . . . . 13 (∃𝑏(𝑏 ∈ (𝑠 “ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩) → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
177165, 176sylbi 207 . . . . . . . . . . . 12 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
178 excom 2039 . . . . . . . . . . . 12 (∃𝑏𝑧(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
179177, 178sylib 208 . . . . . . . . . . 11 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
180 df-rex 2913 . . . . . . . . . . . 12 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
18155elsnres 5395 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑠 ↾ {𝑎}) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠))
182181anbi1i 730 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
183 19.41v 1911 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧))
184 anass 680 . . . . . . . . . . . . . . 15 (((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ (𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
185184exbii 1771 . . . . . . . . . . . . . 14 (∃𝑏((𝑧 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝑎, 𝑏⟩ ∈ 𝑠) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
186182, 183, 1853bitr2i 288 . . . . . . . . . . . . 13 ((𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
187186exbii 1771 . . . . . . . . . . . 12 (∃𝑧(𝑧 ∈ (𝑠 ↾ {𝑎}) ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧) ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
188180, 187bitri 264 . . . . . . . . . . 11 (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 ↔ ∃𝑧𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ (⟨𝑎, 𝑏⟩ ∈ 𝑠 ∧ ∀𝑤𝑠 ¬ 𝑤𝑇𝑧)))
189179, 188sylibr 224 . . . . . . . . . 10 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧)
190 ssrexv 3646 . . . . . . . . . 10 ((𝑠 ↾ {𝑎}) ⊆ 𝑠 → (∃𝑧 ∈ (𝑠 ↾ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑧 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
191164, 189, 190mpsyl 68 . . . . . . . . 9 (∃𝑏 ∈ (𝑠 “ {𝑎})∀𝑤𝑠 ¬ 𝑤𝑇𝑎, 𝑏⟩ → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)
192163, 191syl6 35 . . . . . . . 8 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ((𝑎 ∈ dom 𝑠 ∧ ∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
193192expd 452 . . . . . . 7 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (𝑎 ∈ dom 𝑠 → (∀𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
194193rexlimdv 3023 . . . . . 6 ((𝑆 Fr 𝐵𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
1951943expib 1265 . . . . 5 (𝑆 Fr 𝐵 → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
196195adantl 482 . . . 4 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → (∃𝑎 ∈ dom 𝑠𝑐 ∈ dom 𝑠 ¬ 𝑐𝑅𝑎 → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧)))
19733, 196mpdd 43 . . 3 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
198197alrimiv 1852 . 2 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
199 df-fr 5033 . 2 (𝑇 Fr (𝐴 × 𝐵) ↔ ∀𝑠((𝑠 ⊆ (𝐴 × 𝐵) ∧ 𝑠 ≠ ∅) → ∃𝑧𝑠𝑤𝑠 ¬ 𝑤𝑇𝑧))
200198, 199sylibr 224 1 ((𝑅 Fr 𝐴𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  wss 3555  c0 3891  {csn 4148  cop 4154   class class class wbr 4613  {copab 4672   Fr wfr 5030   × cxp 5072  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  Rel wrel 5079  cfv 5847  1st c1st 7111  2nd c2nd 7112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-int 4441  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-fr 5033  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fv 5855  df-1st 7113  df-2nd 7114
This theorem is referenced by:  wexp  7236
  Copyright terms: Public domain W3C validator