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

Theorem fpwwe2lem12 9716
Description: Lemma for fpwwe2 9718. (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 3353 . . . . . . . . 9 𝑎 ∈ V
32eldm 5489 . . . . . . . 8 (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5 fpwwe2.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ V)
64, 5fpwwe2lem2 9707 . . . . . . . . . . . . 13 (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
76simprbda 492 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)))
87simpld 488 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑎𝐴)
9 selpw 4322 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
108, 9sylibr 225 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
1110ex 401 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
1211exlimdv 2028 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
133, 12syl5bi 233 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊𝑎 ∈ 𝒫 𝐴))
1413ssrdv 3767 . . . . . 6 (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15 sspwuni 4768 . . . . . 6 (dom 𝑊 ⊆ 𝒫 𝐴 dom 𝑊𝐴)
1614, 15sylib 209 . . . . 5 (𝜑 dom 𝑊𝐴)
171, 16syl5eqss 3809 . . . 4 (𝜑𝑋𝐴)
18 vex 3353 . . . . . . . 8 𝑠 ∈ V
1918elrn 5535 . . . . . . 7 (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
207simprd 489 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
214relopabi 5414 . . . . . . . . . . . . . . . 16 Rel 𝑊
2221releldmi 5531 . . . . . . . . . . . . . . 15 (𝑎𝑊𝑠𝑎 ∈ dom 𝑊)
2322adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24 elssuni 4625 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑊𝑎 dom 𝑊)
2523, 24syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎 dom 𝑊)
2625, 1syl6sseqr 3812 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → 𝑎𝑋)
27 xpss12 5292 . . . . . . . . . . . 12 ((𝑎𝑋𝑎𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2826, 26, 27syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2920, 28sstrd 3771 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30 selpw 4322 . . . . . . . . . 10 (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
3129, 30sylibr 225 . . . . . . . . 9 ((𝜑𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
3231ex 401 . . . . . . . 8 (𝜑 → (𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3332exlimdv 2028 . . . . . . 7 (𝜑 → (∃𝑎 𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3419, 33syl5bi 233 . . . . . 6 (𝜑 → (𝑠 ∈ ran 𝑊𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3534ssrdv 3767 . . . . 5 (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36 sspwuni 4768 . . . . 5 (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ran 𝑊 ⊆ (𝑋 × 𝑋))
3735, 36sylib 209 . . . 4 (𝜑 ran 𝑊 ⊆ (𝑋 × 𝑋))
3817, 37jca 507 . . 3 (𝜑 → (𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)))
39 n0 4095 . . . . . . . . 9 (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦𝑛)
40 ssel2 3756 . . . . . . . . . . . . . 14 ((𝑛𝑋𝑦𝑛) → 𝑦𝑋)
4140adantl 473 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → 𝑦𝑋)
421eleq2i 2836 . . . . . . . . . . . . . 14 (𝑦𝑋𝑦 dom 𝑊)
43 eluni2 4598 . . . . . . . . . . . . . 14 (𝑦 dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4442, 43bitri 266 . . . . . . . . . . . . 13 (𝑦𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4541, 44sylib 209 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
462inex2 4961 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ∈ V
4746a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ∈ V)
486simplbda 493 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
4948simpld 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎𝑊𝑠) → 𝑠 We 𝑎)
5049ad2ant2r 753 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 We 𝑎)
51 wefr 5267 . . . . . . . . . . . . . . . . . . 19 (𝑠 We 𝑎𝑠 Fr 𝑎)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 Fr 𝑎)
53 inss2 3993 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ⊆ 𝑎
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ⊆ 𝑎)
55 simplrr 796 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑛)
56 simprr 789 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑎)
57 inelcm 4193 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑛𝑦𝑎) → (𝑛𝑎) ≠ ∅)
5855, 56, 57syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ≠ ∅)
59 fri 5239 . . . . . . . . . . . . . . . . . 18 ((((𝑛𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛𝑎) ⊆ 𝑎 ∧ (𝑛𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
6047, 52, 54, 58, 59syl22anc 867 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
61 simprl 787 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛𝑎))
6261elin1d 3964 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑛)
63 simplrr 796 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
64 ralnex 3139 . . . . . . . . . . . . . . . . . . . 20 (∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
6563, 64sylib 209 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
66 df-br 4810 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ran 𝑊)
67 eluni2 4598 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑤, 𝑣⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
6866, 67bitri 266 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
69 vex 3353 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ V
7069elrn 5535 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71 df-br 4810 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72 simprll 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑛)
7372adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑛)
74 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
75 simp-4l 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
76 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑎𝑊𝑠)
7776ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
78 simprlr 798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
79 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
804, 5fpwwe2lem2 9707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8180adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8279, 81mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
8382simpld 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)))
8483simprd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
8575, 77, 78, 84syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
8685ssbrd 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣𝑤(𝑏 × 𝑏)𝑣))
8774, 86mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88 brxp 5323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤𝑏𝑣𝑏))
8988simplbi 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤(𝑏 × 𝑏)𝑣𝑤𝑏)
9087, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑏)
9190adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
9261elin2d 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑎)
9392ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣𝑎)
94 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95 brinxp2 5348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤𝑏𝑣𝑎) ∧ 𝑤𝑡𝑣))
9691, 93, 94, 95syl21anbrc 1444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
9897breqd 4820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
9996, 98mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
10075, 77, 20syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101100adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102101ssbrd 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑎 × 𝑎)𝑣))
10399, 102mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104 brxp 5323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤𝑎𝑣𝑎))
105104simplbi 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤(𝑎 × 𝑎)𝑣𝑤𝑎)
106103, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
10773, 106elind 3960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛𝑎))
108 breq1 4812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑤 → (𝑧𝑠𝑣𝑤𝑠𝑣))
109108rspcev 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ (𝑛𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
110107, 99, 109syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
11172adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑛)
112 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
11390adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
114112, 113sseldd 3762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
115111, 114elind 3960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛𝑎))
116 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118 inss1 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119117, 118syl6eqss 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
120119ssbrd 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣𝑤𝑠𝑣))
121116, 120mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122115, 121, 109syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
1235adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝐴 ∈ V)
124 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125124adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
1274, 123, 125, 126, 79fpwwe2lem10 9714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
12875, 77, 78, 127syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129110, 122, 128mpjaodan 981 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
130129expr 448 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13171, 130syl5bir 234 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
132131expr 448 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
133132exlimdv 2028 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
13470, 133syl5bi 233 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
135134rexlimdv 3177 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13668, 135syl5bi 233 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑤 ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13765, 136mtod 189 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ 𝑤 ran 𝑊 𝑣)
138137ralrimiva 3113 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
13960, 62, 138reximssdv 3165 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
140139exp32 411 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
141140exlimdv 2028 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
1423, 141syl5bi 233 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
143142rexlimdv 3177 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14445, 143mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
145144expr 448 . . . . . . . . . 10 ((𝜑𝑛𝑋) → (𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
146145exlimdv 2028 . . . . . . . . 9 ((𝜑𝑛𝑋) → (∃𝑦 𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14739, 146syl5bi 233 . . . . . . . 8 ((𝜑𝑛𝑋) → (𝑛 ≠ ∅ → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
148147expimpd 445 . . . . . . 7 (𝜑 → ((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
149148alrimiv 2022 . . . . . 6 (𝜑 → ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
150 df-fr 5236 . . . . . 6 ( ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
151149, 150sylibr 225 . . . . 5 (𝜑 ran 𝑊 Fr 𝑋)
1521eleq2i 2836 . . . . . . . . . 10 (𝑤𝑋𝑤 dom 𝑊)
153 eluni2 4598 . . . . . . . . . 10 (𝑤 dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
154152, 153bitri 266 . . . . . . . . 9 (𝑤𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
15544, 154anbi12i 620 . . . . . . . 8 ((𝑦𝑋𝑤𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
156 reeanv 3254 . . . . . . . 8 (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
157155, 156bitr4i 269 . . . . . . 7 ((𝑦𝑋𝑤𝑋) ↔ ∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏))
158 vex 3353 . . . . . . . . . . . 12 𝑏 ∈ V
159158eldm 5489 . . . . . . . . . . 11 (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
1603, 159anbi12i 620 . . . . . . . . . 10 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161 eeanv 2346 . . . . . . . . . 10 (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162160, 161bitr4i 269 . . . . . . . . 9 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ ∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡))
16382simprd 489 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164163simpld 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165164ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166 weso 5268 . . . . . . . . . . . . . . 15 (𝑡 We 𝑏𝑡 Or 𝑏)
167165, 166syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168 simprl 787 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎𝑏)
169 simplrl 795 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑎)
170168, 169sseldd 3762 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑏)
171 simplrr 796 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
172 solin 5221 . . . . . . . . . . . . . 14 ((𝑡 Or 𝑏 ∧ (𝑦𝑏𝑤𝑏)) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
173167, 170, 171, 172syl12anc 865 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
17421relelrni 5532 . . . . . . . . . . . . . . . . . 18 (𝑏𝑊𝑡𝑡 ∈ ran 𝑊)
175174ad2antll 720 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176175ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177 elssuni 4625 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ran 𝑊𝑡 ran 𝑊)
178176, 177syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ran 𝑊)
179178ssbrd 4852 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 ran 𝑊 𝑤))
180 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤𝑦 = 𝑤))
181178ssbrd 4852 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦𝑤 ran 𝑊 𝑦))
182179, 180, 1813orim123d 1568 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
183173, 182mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
18449adantrr 708 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 We 𝑎)
185184ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
186 weso 5268 . . . . . . . . . . . . . . 15 (𝑠 We 𝑎𝑠 Or 𝑎)
187185, 186syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
188 simplrl 795 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦𝑎)
189 simprl 787 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
190 simplrr 796 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
191189, 190sseldd 3762 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
192 solin 5221 . . . . . . . . . . . . . 14 ((𝑠 Or 𝑎 ∧ (𝑦𝑎𝑤𝑎)) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
193187, 188, 191, 192syl12anc 865 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
19421relelrni 5532 . . . . . . . . . . . . . . . . . 18 (𝑎𝑊𝑠𝑠 ∈ ran 𝑊)
195194ad2antrl 719 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196195ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197 elssuni 4625 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ran 𝑊𝑠 ran 𝑊)
198196, 197syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ran 𝑊)
199198ssbrd 4852 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 ran 𝑊 𝑤))
200 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤𝑦 = 𝑤))
201198ssbrd 4852 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦𝑤 ran 𝑊 𝑦))
202199, 200, 2013orim123d 1568 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
203193, 202mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
204127adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205183, 203, 204mpjaodan 981 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
206205exp31 410 . . . . . . . . . 10 (𝜑 → ((𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
207206exlimdvv 2029 . . . . . . . . 9 (𝜑 → (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
208162, 207syl5bi 233 . . . . . . . 8 (𝜑 → ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
209208rexlimdvv 3184 . . . . . . 7 (𝜑 → (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
210157, 209syl5bi 233 . . . . . 6 (𝜑 → ((𝑦𝑋𝑤𝑋) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
211210ralrimivv 3117 . . . . 5 (𝜑 → ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
212 dfwe2 7179 . . . . 5 ( ran 𝑊 We 𝑋 ↔ ( ran 𝑊 Fr 𝑋 ∧ ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
213151, 211, 212sylanbrc 578 . . . 4 (𝜑 ran 𝑊 We 𝑋)
2144fpwwe2cbv 9705 . . . . . . . . . . . . 13 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧𝐴𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤𝑧 [(𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
2155adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝐴 ∈ V)
216 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217214, 215, 216fpwwe2lem3 9708 . . . . . . . . . . . 12 (((𝜑𝑎𝑊𝑠) ∧ 𝑦𝑎) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
218217anasss 458 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
219 cnvimass 5667 . . . . . . . . . . . . 13 ( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊
2205, 17ssexd 4966 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ V)
221 xpexg 7158 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V)
222220, 220, 221syl2anc 579 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 × 𝑋) ∈ V)
223222, 37ssexd 4966 . . . . . . . . . . . . . . 15 (𝜑 ran 𝑊 ∈ V)
224223adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ran 𝑊 ∈ V)
225 dmexg 7295 . . . . . . . . . . . . . 14 ( ran 𝑊 ∈ V → dom ran 𝑊 ∈ V)
226224, 225syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → dom ran 𝑊 ∈ V)
227 ssexg 4965 . . . . . . . . . . . . 13 ((( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊 ∧ dom ran 𝑊 ∈ V) → ( ran 𝑊 “ {𝑦}) ∈ V)
228219, 226, 227sylancr 581 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) ∈ V)
229 id 22 . . . . . . . . . . . . . . 15 (𝑢 = ( ran 𝑊 “ {𝑦}) → 𝑢 = ( ran 𝑊 “ {𝑦}))
230 olc 894 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
231 df-br 4810 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ran 𝑊)
232 eluni2 4598 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑧, 𝑤⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
233231, 232bitri 266 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
234 df-br 4810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
23584ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
236235ssbrd 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑏)𝑤))
237 brxp 5323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧𝑏𝑤𝑏))
238237simplbi 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑧(𝑏 × 𝑏)𝑤𝑧𝑏)
239236, 238syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑏))
24020adantrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
241240ssbrd 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑤𝑠𝑦𝑤(𝑎 × 𝑎)𝑦))
242241imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
243 brxp 5323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤𝑎𝑦𝑎))
244243simplbi 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤(𝑎 × 𝑎)𝑦𝑤𝑎)
245242, 244syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤𝑎)
246245a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦𝑎𝑤𝑎))
247 elequ1 2162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤 = 𝑦 → (𝑤𝑎𝑦𝑎))
248247biimprd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑤 = 𝑦 → (𝑦𝑎𝑤𝑎))
249248adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦𝑎𝑤𝑎))
250246, 249jaodan 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑦𝑎𝑤𝑎))
251250impr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → 𝑤𝑎)
252251adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
253239, 252jctird 522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑏𝑤𝑎)))
254 brxp 5323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧𝑏𝑤𝑎))
255253, 254syl6ibr 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
256255ancld 546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
257 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
258257breqd 4820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
259 brin 4861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
260258, 259syl6bb 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
261256, 260sylibrd 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
262 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
263262, 118syl6eqss 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
264263ssbrd 4852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
265127adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
266261, 264, 265mpjaodan 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (𝑧𝑡𝑤𝑧𝑠𝑤))
267234, 266syl5bir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
268267exp32 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
269268expr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
270269com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑎𝑊𝑠) → (𝑦𝑎 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
271270impr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
272271imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
273272exlimdv 2028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
27470, 273syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
275274rexlimdv 3177 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
276233, 275syl5bi 233 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
277230, 276sylan2 586 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤 = 𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
278277ex 401 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
279278alrimiv 2022 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
280 breq2 4813 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧 ran 𝑊 𝑦))
281 breq2 4813 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧𝑠𝑤𝑧𝑠𝑦))
282280, 281imbi12d 335 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → ((𝑧 ran 𝑊 𝑤𝑧𝑠𝑤) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦)))
283282equsalvw 2101 . . . . . . . . . . . . . . . . . . 19 (∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
284279, 283sylib 209 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
285194ad2antrl 719 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ∈ ran 𝑊)
286285, 197syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ran 𝑊)
287286ssbrd 4852 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧𝑠𝑦𝑧 ran 𝑊 𝑦))
288284, 287impbid 203 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
289 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
290289eliniseg 5676 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦))
291290elv 3354 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦)
292289eliniseg 5676 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
293292elv 3354 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
294288, 291, 2933bitr4g 305 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (𝑠 “ {𝑦})))
295294eqrdv 2763 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) = (𝑠 “ {𝑦}))
296229, 295sylan9eqr 2821 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → 𝑢 = (𝑠 “ {𝑦}))
297296sqxpeqd 5309 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
298297ineq2d 3976 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
299 relinxp 5406 . . . . . . . . . . . . . . . . 17 Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
300 relinxp 5406 . . . . . . . . . . . . . . . . 17 Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
301 vex 3353 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
302301eliniseg 5676 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ V → (𝑤 ∈ (𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
303292, 302anbi12d 624 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ V → ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦)))
304303elv 3354 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦))
305 orc 893 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑠𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
306305, 276sylan2 586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
307306adantrl 707 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
308286adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → 𝑠 ran 𝑊)
309308ssbrd 4852 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧𝑠𝑤𝑧 ran 𝑊 𝑤))
310307, 309impbid 203 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
311304, 310sylan2b 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}))) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
312311pm5.32da 574 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
313 df-br 4810 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
314 brinxp2 5348 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
315313, 314bitr3i 268 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
316 df-br 4810 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
317 brinxp2 5348 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
318316, 317bitr3i 268 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
319312, 315, 3183bitr4g 305 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
320299, 300, 319eqrelrdv 5385 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
321320adantr 472 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
322298, 321eqtrd 2799 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
323296, 322oveq12d 6860 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
324323eqeq1d 2767 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ((𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
325228, 324sbcied 3633 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ([( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
326218, 325mpbird 248 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
327326exp32 411 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328327exlimdv 2028 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
3293, 328syl5bi 233 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
330329rexlimdv 3177 . . . . . 6 (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
33144, 330syl5bi 233 . . . . 5 (𝜑 → (𝑦𝑋[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
332331ralrimiv 3112 . . . 4 (𝜑 → ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
333213, 332jca 507 . . 3 (𝜑 → ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
3344, 5fpwwe2lem2 9707 . . 3 (𝜑 → (𝑋𝑊 ran 𝑊 ↔ ((𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
33538, 333, 334mpbir2and 704 . 2 (𝜑𝑋𝑊 ran 𝑊)
33621releldmi 5531 . 2 (𝑋𝑊 ran 𝑊𝑋 ∈ dom 𝑊)
337335, 336syl 17 1 (𝜑𝑋 ∈ dom 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3o 1106  w3a 1107  wal 1650   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  [wsbc 3596  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315  {csn 4334  cop 4340   cuni 4594   class class class wbr 4809  {copab 4871   Or wor 5197   Fr wfr 5233   We wwe 5235   × cxp 5275  ccnv 5276  dom cdm 5277  ran crn 5278  cima 5280  (class class class)co 6842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-wrecs 7610  df-recs 7672  df-oi 8622
This theorem is referenced by:  fpwwe2lem13  9717  fpwwe2  9718
  Copyright terms: Public domain W3C validator