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

Theorem fpwwe2lem12 10062
Description: Lemma for fpwwe2 10064. (Contributed by Mario Carneiro, 18-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
fpwwe2.3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2.4 𝑋 = dom 𝑊
Assertion
Ref Expression
fpwwe2lem12 (𝜑𝑋 ∈ dom 𝑊)
Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem12
Dummy variables 𝑎 𝑏 𝑠 𝑡 𝑣 𝑤 𝑧 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2.4 . . . . 5 𝑋 = dom 𝑊
2 vex 3497 . . . . . . . . 9 𝑎 ∈ V
32eldm 5768 . . . . . . . 8 (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5 fpwwe2.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ V)
64, 5fpwwe2lem2 10053 . . . . . . . . . . . . 13 (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
76simprbda 501 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)))
87simpld 497 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑎𝐴)
9 velpw 4543 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
108, 9sylibr 236 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
1110ex 415 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
1211exlimdv 1930 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
133, 12syl5bi 244 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊𝑎 ∈ 𝒫 𝐴))
1413ssrdv 3972 . . . . . 6 (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15 sspwuni 5021 . . . . . 6 (dom 𝑊 ⊆ 𝒫 𝐴 dom 𝑊𝐴)
1614, 15sylib 220 . . . . 5 (𝜑 dom 𝑊𝐴)
171, 16eqsstrid 4014 . . . 4 (𝜑𝑋𝐴)
18 vex 3497 . . . . . . . 8 𝑠 ∈ V
1918elrn 5821 . . . . . . 7 (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
207simprd 498 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
214relopabi 5693 . . . . . . . . . . . . . . . 16 Rel 𝑊
2221releldmi 5817 . . . . . . . . . . . . . . 15 (𝑎𝑊𝑠𝑎 ∈ dom 𝑊)
2322adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24 elssuni 4867 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑊𝑎 dom 𝑊)
2523, 24syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎 dom 𝑊)
2625, 1sseqtrrdi 4017 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → 𝑎𝑋)
27 xpss12 5569 . . . . . . . . . . . 12 ((𝑎𝑋𝑎𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2826, 26, 27syl2anc 586 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2920, 28sstrd 3976 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30 velpw 4543 . . . . . . . . . 10 (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
3129, 30sylibr 236 . . . . . . . . 9 ((𝜑𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
3231ex 415 . . . . . . . 8 (𝜑 → (𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3332exlimdv 1930 . . . . . . 7 (𝜑 → (∃𝑎 𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3419, 33syl5bi 244 . . . . . 6 (𝜑 → (𝑠 ∈ ran 𝑊𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3534ssrdv 3972 . . . . 5 (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36 sspwuni 5021 . . . . 5 (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ran 𝑊 ⊆ (𝑋 × 𝑋))
3735, 36sylib 220 . . . 4 (𝜑 ran 𝑊 ⊆ (𝑋 × 𝑋))
3817, 37jca 514 . . 3 (𝜑 → (𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)))
39 n0 4309 . . . . . . . . 9 (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦𝑛)
40 ssel2 3961 . . . . . . . . . . . . . 14 ((𝑛𝑋𝑦𝑛) → 𝑦𝑋)
4140adantl 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → 𝑦𝑋)
421eleq2i 2904 . . . . . . . . . . . . . 14 (𝑦𝑋𝑦 dom 𝑊)
43 eluni2 4841 . . . . . . . . . . . . . 14 (𝑦 dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4442, 43bitri 277 . . . . . . . . . . . . 13 (𝑦𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4541, 44sylib 220 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
462inex2 5221 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ∈ V
4746a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ∈ V)
486simplbda 502 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
4948simpld 497 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎𝑊𝑠) → 𝑠 We 𝑎)
5049ad2ant2r 745 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 We 𝑎)
51 wefr 5544 . . . . . . . . . . . . . . . . . . 19 (𝑠 We 𝑎𝑠 Fr 𝑎)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 Fr 𝑎)
53 inss2 4205 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ⊆ 𝑎
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ⊆ 𝑎)
55 simplrr 776 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑛)
56 simprr 771 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑎)
57 inelcm 4413 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑛𝑦𝑎) → (𝑛𝑎) ≠ ∅)
5855, 56, 57syl2anc 586 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ≠ ∅)
59 fri 5516 . . . . . . . . . . . . . . . . . 18 ((((𝑛𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛𝑎) ⊆ 𝑎 ∧ (𝑛𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
6047, 52, 54, 58, 59syl22anc 836 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
61 simprl 769 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛𝑎))
6261elin1d 4174 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑛)
63 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
64 ralnex 3236 . . . . . . . . . . . . . . . . . . . 20 (∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
6563, 64sylib 220 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
66 df-br 5066 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ran 𝑊)
67 eluni2 4841 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑤, 𝑣⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
6866, 67bitri 277 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
69 vex 3497 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ V
7069elrn 5821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71 df-br 5066 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72 simprll 777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑛)
7372adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑛)
74 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
75 simp-4l 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
76 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑎𝑊𝑠)
7776ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
78 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
79 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
804, 5fpwwe2lem2 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8180adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8279, 81mpbid 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
8382simpld 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)))
8483simprd 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
8575, 77, 78, 84syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
8685ssbrd 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣𝑤(𝑏 × 𝑏)𝑣))
8774, 86mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88 brxp 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤𝑏𝑣𝑏))
8988simplbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤(𝑏 × 𝑏)𝑣𝑤𝑏)
9087, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑏)
9190adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
9261elin2d 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑎)
9392ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣𝑎)
94 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95 brinxp2 5628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤𝑏𝑣𝑎) ∧ 𝑤𝑡𝑣))
9691, 93, 94, 95syl21anbrc 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
9897breqd 5076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
9996, 98mpbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
10075, 77, 20syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101100adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102101ssbrd 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑎 × 𝑎)𝑣))
10399, 102mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104 brxp 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤𝑎𝑣𝑎))
105104simplbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤(𝑎 × 𝑎)𝑣𝑤𝑎)
106103, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
10773, 106elind 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛𝑎))
108 breq1 5068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑤 → (𝑧𝑠𝑣𝑤𝑠𝑣))
109108rspcev 3622 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ (𝑛𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
110107, 99, 109syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
11172adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑛)
112 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
11390adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
114112, 113sseldd 3967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
115111, 114elind 4170 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛𝑎))
116 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118 inss1 4204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119117, 118eqsstrdi 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
120119ssbrd 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣𝑤𝑠𝑣))
121116, 120mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122115, 121, 109syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
1235adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝐴 ∈ V)
124 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125124adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
1274, 123, 125, 126, 79fpwwe2lem10 10060 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
12875, 77, 78, 127syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129110, 122, 128mpjaodan 955 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
130129expr 459 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13171, 130syl5bir 245 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
132131expr 459 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
133132exlimdv 1930 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
13470, 133syl5bi 244 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
135134rexlimdv 3283 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13668, 135syl5bi 244 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑤 ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13765, 136mtod 200 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ 𝑤 ran 𝑊 𝑣)
138137ralrimiva 3182 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
13960, 62, 138reximssdv 3276 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
140139exp32 423 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
141140exlimdv 1930 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
1423, 141syl5bi 244 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
143142rexlimdv 3283 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14445, 143mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
145144expr 459 . . . . . . . . . 10 ((𝜑𝑛𝑋) → (𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
146145exlimdv 1930 . . . . . . . . 9 ((𝜑𝑛𝑋) → (∃𝑦 𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14739, 146syl5bi 244 . . . . . . . 8 ((𝜑𝑛𝑋) → (𝑛 ≠ ∅ → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
148147expimpd 456 . . . . . . 7 (𝜑 → ((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
149148alrimiv 1924 . . . . . 6 (𝜑 → ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
150 df-fr 5513 . . . . . 6 ( ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
151149, 150sylibr 236 . . . . 5 (𝜑 ran 𝑊 Fr 𝑋)
1521eleq2i 2904 . . . . . . . . . 10 (𝑤𝑋𝑤 dom 𝑊)
153 eluni2 4841 . . . . . . . . . 10 (𝑤 dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
154152, 153bitri 277 . . . . . . . . 9 (𝑤𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
15544, 154anbi12i 628 . . . . . . . 8 ((𝑦𝑋𝑤𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
156 reeanv 3367 . . . . . . . 8 (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
157155, 156bitr4i 280 . . . . . . 7 ((𝑦𝑋𝑤𝑋) ↔ ∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏))
158 vex 3497 . . . . . . . . . . . 12 𝑏 ∈ V
159158eldm 5768 . . . . . . . . . . 11 (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
1603, 159anbi12i 628 . . . . . . . . . 10 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161 exdistrv 1952 . . . . . . . . . 10 (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162160, 161bitr4i 280 . . . . . . . . 9 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ ∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡))
16382simprd 498 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164163simpld 497 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165164ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166 weso 5545 . . . . . . . . . . . . . . 15 (𝑡 We 𝑏𝑡 Or 𝑏)
167165, 166syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168 simprl 769 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎𝑏)
169 simplrl 775 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑎)
170168, 169sseldd 3967 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑏)
171 simplrr 776 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
172 solin 5497 . . . . . . . . . . . . . 14 ((𝑡 Or 𝑏 ∧ (𝑦𝑏𝑤𝑏)) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
173167, 170, 171, 172syl12anc 834 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
17421relelrni 5818 . . . . . . . . . . . . . . . . . 18 (𝑏𝑊𝑡𝑡 ∈ ran 𝑊)
175174ad2antll 727 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176175ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177 elssuni 4867 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ran 𝑊𝑡 ran 𝑊)
178176, 177syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ran 𝑊)
179178ssbrd 5108 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 ran 𝑊 𝑤))
180 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤𝑦 = 𝑤))
181178ssbrd 5108 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦𝑤 ran 𝑊 𝑦))
182179, 180, 1813orim123d 1440 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
183173, 182mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
18449adantrr 715 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 We 𝑎)
185184ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
186 weso 5545 . . . . . . . . . . . . . . 15 (𝑠 We 𝑎𝑠 Or 𝑎)
187185, 186syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
188 simplrl 775 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦𝑎)
189 simprl 769 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
190 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
191189, 190sseldd 3967 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
192 solin 5497 . . . . . . . . . . . . . 14 ((𝑠 Or 𝑎 ∧ (𝑦𝑎𝑤𝑎)) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
193187, 188, 191, 192syl12anc 834 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
19421relelrni 5818 . . . . . . . . . . . . . . . . . 18 (𝑎𝑊𝑠𝑠 ∈ ran 𝑊)
195194ad2antrl 726 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196195ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197 elssuni 4867 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ran 𝑊𝑠 ran 𝑊)
198196, 197syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ran 𝑊)
199198ssbrd 5108 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 ran 𝑊 𝑤))
200 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤𝑦 = 𝑤))
201198ssbrd 5108 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦𝑤 ran 𝑊 𝑦))
202199, 200, 2013orim123d 1440 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
203193, 202mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
204127adantr 483 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205183, 203, 204mpjaodan 955 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
206205exp31 422 . . . . . . . . . 10 (𝜑 → ((𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
207206exlimdvv 1931 . . . . . . . . 9 (𝜑 → (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
208162, 207syl5bi 244 . . . . . . . 8 (𝜑 → ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
209208rexlimdvv 3293 . . . . . . 7 (𝜑 → (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
210157, 209syl5bi 244 . . . . . 6 (𝜑 → ((𝑦𝑋𝑤𝑋) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
211210ralrimivv 3190 . . . . 5 (𝜑 → ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
212 dfwe2 7495 . . . . 5 ( ran 𝑊 We 𝑋 ↔ ( ran 𝑊 Fr 𝑋 ∧ ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
213151, 211, 212sylanbrc 585 . . . 4 (𝜑 ran 𝑊 We 𝑋)
2144fpwwe2cbv 10051 . . . . . . . . . . . . 13 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧𝐴𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤𝑧 [(𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
2155adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝐴 ∈ V)
216 simpr 487 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217214, 215, 216fpwwe2lem3 10054 . . . . . . . . . . . 12 (((𝜑𝑎𝑊𝑠) ∧ 𝑦𝑎) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
218217anasss 469 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
219 cnvimass 5948 . . . . . . . . . . . . 13 ( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊
2205, 17ssexd 5227 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ V)
221220, 220xpexd 7473 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 × 𝑋) ∈ V)
222221, 37ssexd 5227 . . . . . . . . . . . . . . 15 (𝜑 ran 𝑊 ∈ V)
223222adantr 483 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ran 𝑊 ∈ V)
224223dmexd 7614 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → dom ran 𝑊 ∈ V)
225 ssexg 5226 . . . . . . . . . . . . 13 ((( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊 ∧ dom ran 𝑊 ∈ V) → ( ran 𝑊 “ {𝑦}) ∈ V)
226219, 224, 225sylancr 589 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) ∈ V)
227 id 22 . . . . . . . . . . . . . . 15 (𝑢 = ( ran 𝑊 “ {𝑦}) → 𝑢 = ( ran 𝑊 “ {𝑦}))
228 olc 864 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
229 df-br 5066 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ran 𝑊)
230 eluni2 4841 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑧, 𝑤⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
231229, 230bitri 277 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
232 df-br 5066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
23384ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
234233ssbrd 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑏)𝑤))
235 brxp 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧𝑏𝑤𝑏))
236235simplbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑧(𝑏 × 𝑏)𝑤𝑧𝑏)
237234, 236syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑏))
23820adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
239238ssbrd 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑤𝑠𝑦𝑤(𝑎 × 𝑎)𝑦))
240239imp 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
241 brxp 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤𝑎𝑦𝑎))
242241simplbi 500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤(𝑎 × 𝑎)𝑦𝑤𝑎)
243240, 242syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤𝑎)
244243a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦𝑎𝑤𝑎))
245 elequ1 2117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤 = 𝑦 → (𝑤𝑎𝑦𝑎))
246245biimprd 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑤 = 𝑦 → (𝑦𝑎𝑤𝑎))
247246adantl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦𝑎𝑤𝑎))
248244, 247jaodan 954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑦𝑎𝑤𝑎))
249248impr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → 𝑤𝑎)
250249adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
251237, 250jctird 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑏𝑤𝑎)))
252 brxp 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧𝑏𝑤𝑎))
253251, 252syl6ibr 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
254253ancld 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
255 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
256255breqd 5076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
257 brin 5117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
258256, 257syl6bb 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
259254, 258sylibrd 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
260 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
261260, 118eqsstrdi 4020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
262261ssbrd 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
263127adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
264259, 262, 263mpjaodan 955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (𝑧𝑡𝑤𝑧𝑠𝑤))
265232, 264syl5bir 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
266265exp32 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
267266expr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
268267com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑎𝑊𝑠) → (𝑦𝑎 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
269268impr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
270269imp 409 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
271270exlimdv 1930 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
27270, 271syl5bi 244 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
273272rexlimdv 3283 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
274231, 273syl5bi 244 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
275228, 274sylan2 594 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤 = 𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
276275ex 415 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
277276alrimiv 1924 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
278 breq2 5069 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧 ran 𝑊 𝑦))
279 breq2 5069 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧𝑠𝑤𝑧𝑠𝑦))
280278, 279imbi12d 347 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → ((𝑧 ran 𝑊 𝑤𝑧𝑠𝑤) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦)))
281280equsalvw 2006 . . . . . . . . . . . . . . . . . . 19 (∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
282277, 281sylib 220 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
283194ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ∈ ran 𝑊)
284283, 197syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ran 𝑊)
285284ssbrd 5108 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧𝑠𝑦𝑧 ran 𝑊 𝑦))
286282, 285impbid 214 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
287 vex 3497 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
288287eliniseg 5957 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦))
289288elv 3499 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦)
290287eliniseg 5957 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
291290elv 3499 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
292286, 289, 2913bitr4g 316 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (𝑠 “ {𝑦})))
293292eqrdv 2819 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) = (𝑠 “ {𝑦}))
294227, 293sylan9eqr 2878 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → 𝑢 = (𝑠 “ {𝑦}))
295294sqxpeqd 5586 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
296295ineq2d 4188 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
297 relinxp 5686 . . . . . . . . . . . . . . . . 17 Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
298 relinxp 5686 . . . . . . . . . . . . . . . . 17 Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
299 vex 3497 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
300299eliniseg 5957 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ V → (𝑤 ∈ (𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
301290, 300anbi12d 632 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ V → ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦)))
302301elv 3499 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦))
303 orc 863 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑠𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
304303, 274sylan2 594 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
305304adantrl 714 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
306284adantr 483 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → 𝑠 ran 𝑊)
307306ssbrd 5108 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧𝑠𝑤𝑧 ran 𝑊 𝑤))
308305, 307impbid 214 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
309302, 308sylan2b 595 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}))) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
310309pm5.32da 581 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
311 df-br 5066 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
312 brinxp2 5628 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
313311, 312bitr3i 279 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
314 df-br 5066 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
315 brinxp2 5628 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
316314, 315bitr3i 279 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
317310, 313, 3163bitr4g 316 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
318297, 298, 317eqrelrdv 5664 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
319318adantr 483 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
320296, 319eqtrd 2856 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
321294, 320oveq12d 7173 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
322321eqeq1d 2823 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ((𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
323226, 322sbcied 3813 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ([( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
324218, 323mpbird 259 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
325324exp32 423 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
326325exlimdv 1930 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
3273, 326syl5bi 244 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328327rexlimdv 3283 . . . . . 6 (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
32944, 328syl5bi 244 . . . . 5 (𝜑 → (𝑦𝑋[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
330329ralrimiv 3181 . . . 4 (𝜑 → ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
331213, 330jca 514 . . 3 (𝜑 → ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
3324, 5fpwwe2lem2 10053 . . 3 (𝜑 → (𝑋𝑊 ran 𝑊 ↔ ((𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
33338, 331, 332mpbir2and 711 . 2 (𝜑𝑋𝑊 ran 𝑊)
33421releldmi 5817 . 2 (𝑋𝑊 ran 𝑊𝑋 ∈ dom 𝑊)
335333, 334syl 17 1 (𝜑𝑋 ∈ dom 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3o 1082  w3a 1083  wal 1531   = wceq 1533  wex 1776  wcel 2110  wne 3016  wral 3138  wrex 3139  Vcvv 3494  [wsbc 3771  cin 3934  wss 3935  c0 4290  𝒫 cpw 4538  {csn 4566  cop 4572   cuni 4837   class class class wbr 5065  {copab 5127   Or wor 5472   Fr wfr 5510   We wwe 5512   × cxp 5552  ccnv 5553  dom cdm 5554  ran crn 5555  cima 5557  (class class class)co 7155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7113  df-ov 7158  df-wrecs 7946  df-recs 8007  df-oi 8973
This theorem is referenced by:  fpwwe2lem13  10063  fpwwe2  10064
  Copyright terms: Public domain W3C validator