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

Theorem fpwwe2lem12 9785
 Description: Lemma for fpwwe2 9787. (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 3417 . . . . . . . . 9 𝑎 ∈ V
32eldm 5557 . . . . . . . 8 (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5 fpwwe2.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ V)
64, 5fpwwe2lem2 9776 . . . . . . . . . . . . 13 (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
76simprbda 494 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)))
87simpld 490 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑎𝐴)
9 selpw 4387 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
108, 9sylibr 226 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
1110ex 403 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
1211exlimdv 2032 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
133, 12syl5bi 234 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊𝑎 ∈ 𝒫 𝐴))
1413ssrdv 3833 . . . . . 6 (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15 sspwuni 4834 . . . . . 6 (dom 𝑊 ⊆ 𝒫 𝐴 dom 𝑊𝐴)
1614, 15sylib 210 . . . . 5 (𝜑 dom 𝑊𝐴)
171, 16syl5eqss 3874 . . . 4 (𝜑𝑋𝐴)
18 vex 3417 . . . . . . . 8 𝑠 ∈ V
1918elrn 5603 . . . . . . 7 (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
207simprd 491 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
214relopabi 5482 . . . . . . . . . . . . . . . 16 Rel 𝑊
2221releldmi 5599 . . . . . . . . . . . . . . 15 (𝑎𝑊𝑠𝑎 ∈ dom 𝑊)
2322adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24 elssuni 4691 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑊𝑎 dom 𝑊)
2523, 24syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎 dom 𝑊)
2625, 1syl6sseqr 3877 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → 𝑎𝑋)
27 xpss12 5361 . . . . . . . . . . . 12 ((𝑎𝑋𝑎𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2826, 26, 27syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2920, 28sstrd 3837 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30 selpw 4387 . . . . . . . . . 10 (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
3129, 30sylibr 226 . . . . . . . . 9 ((𝜑𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
3231ex 403 . . . . . . . 8 (𝜑 → (𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3332exlimdv 2032 . . . . . . 7 (𝜑 → (∃𝑎 𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3419, 33syl5bi 234 . . . . . 6 (𝜑 → (𝑠 ∈ ran 𝑊𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3534ssrdv 3833 . . . . 5 (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36 sspwuni 4834 . . . . 5 (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ran 𝑊 ⊆ (𝑋 × 𝑋))
3735, 36sylib 210 . . . 4 (𝜑 ran 𝑊 ⊆ (𝑋 × 𝑋))
3817, 37jca 507 . . 3 (𝜑 → (𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)))
39 n0 4162 . . . . . . . . 9 (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦𝑛)
40 ssel2 3822 . . . . . . . . . . . . . 14 ((𝑛𝑋𝑦𝑛) → 𝑦𝑋)
4140adantl 475 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → 𝑦𝑋)
421eleq2i 2898 . . . . . . . . . . . . . 14 (𝑦𝑋𝑦 dom 𝑊)
43 eluni2 4664 . . . . . . . . . . . . . 14 (𝑦 dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4442, 43bitri 267 . . . . . . . . . . . . 13 (𝑦𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4541, 44sylib 210 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
462inex2 5027 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ∈ V
4746a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ∈ V)
486simplbda 495 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
4948simpld 490 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎𝑊𝑠) → 𝑠 We 𝑎)
5049ad2ant2r 753 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 We 𝑎)
51 wefr 5336 . . . . . . . . . . . . . . . . . . 19 (𝑠 We 𝑎𝑠 Fr 𝑎)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 Fr 𝑎)
53 inss2 4060 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ⊆ 𝑎
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ⊆ 𝑎)
55 simplrr 796 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑛)
56 simprr 789 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑎)
57 inelcm 4258 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑛𝑦𝑎) → (𝑛𝑎) ≠ ∅)
5855, 56, 57syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ≠ ∅)
59 fri 5308 . . . . . . . . . . . . . . . . . 18 ((((𝑛𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛𝑎) ⊆ 𝑎 ∧ (𝑛𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
6047, 52, 54, 58, 59syl22anc 872 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
61 simprl 787 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛𝑎))
6261elin1d 4031 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑛)
63 simplrr 796 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
64 ralnex 3201 . . . . . . . . . . . . . . . . . . . 20 (∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
6563, 64sylib 210 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
66 df-br 4876 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ran 𝑊)
67 eluni2 4664 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑤, 𝑣⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
6866, 67bitri 267 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
69 vex 3417 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ V
7069elrn 5603 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
71 df-br 4876 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
72 simprll 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑛)
7372adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8180adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8279, 81mpbid 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
8382simpld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)))
8483simprd 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
8575, 77, 78, 84syl12anc 870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
8685ssbrd 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣𝑤(𝑏 × 𝑏)𝑣))
8774, 86mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
88 brxp 5392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤𝑏𝑣𝑏))
8988simplbi 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑤(𝑏 × 𝑏)𝑣𝑤𝑏)
9087, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑏)
9190adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
9261elin2d 4032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑎)
9392ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣𝑎)
94 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
95 brinxp2 5417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ ((𝑤𝑏𝑣𝑎) ∧ 𝑤𝑡𝑣))
9691, 93, 94, 95syl21anbrc 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
97 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
9897breqd 4886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
9996, 98mpbird 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
10075, 77, 20syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
101100adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
102101ssbrd 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑎 × 𝑎)𝑣))
10399, 102mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
104 brxp 5392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤𝑎𝑣𝑎))
105104simplbi 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑤(𝑎 × 𝑎)𝑣𝑤𝑎)
106103, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
10773, 106elind 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛𝑎))
108 breq1 4878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑤 → (𝑧𝑠𝑣𝑤𝑠𝑣))
109108rspcev 3526 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤 ∈ (𝑛𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
110107, 99, 109syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
11172adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑛)
112 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
11390adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
114112, 113sseldd 3828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
115111, 114elind 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛𝑎))
116 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
117 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
118 inss1 4059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
119117, 118syl6eqss 3880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
120119ssbrd 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣𝑤𝑠𝑣))
121116, 120mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
122115, 121, 109syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
1235adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝐴 ∈ V)
124 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
125124adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
1274, 123, 125, 126, 79fpwwe2lem10 9783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
12875, 77, 78, 127syl12anc 870 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
129110, 122, 128mpjaodan 986 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
130129expr 450 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13171, 130syl5bir 235 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
132131expr 450 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
133132exlimdv 2032 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
13470, 133syl5bi 234 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
135134rexlimdv 3239 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13668, 135syl5bi 234 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑤 ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13765, 136mtod 190 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ 𝑤 ran 𝑊 𝑣)
138137ralrimiva 3175 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
13960, 62, 138reximssdv 3227 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
140139exp32 413 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
141140exlimdv 2032 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
1423, 141syl5bi 234 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
143142rexlimdv 3239 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14445, 143mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
145144expr 450 . . . . . . . . . 10 ((𝜑𝑛𝑋) → (𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
146145exlimdv 2032 . . . . . . . . 9 ((𝜑𝑛𝑋) → (∃𝑦 𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14739, 146syl5bi 234 . . . . . . . 8 ((𝜑𝑛𝑋) → (𝑛 ≠ ∅ → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
148147expimpd 447 . . . . . . 7 (𝜑 → ((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
149148alrimiv 2026 . . . . . 6 (𝜑 → ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
150 df-fr 5305 . . . . . 6 ( ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
151149, 150sylibr 226 . . . . 5 (𝜑 ran 𝑊 Fr 𝑋)
1521eleq2i 2898 . . . . . . . . . 10 (𝑤𝑋𝑤 dom 𝑊)
153 eluni2 4664 . . . . . . . . . 10 (𝑤 dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
154152, 153bitri 267 . . . . . . . . 9 (𝑤𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
15544, 154anbi12i 620 . . . . . . . 8 ((𝑦𝑋𝑤𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
156 reeanv 3317 . . . . . . . 8 (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
157155, 156bitr4i 270 . . . . . . 7 ((𝑦𝑋𝑤𝑋) ↔ ∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏))
158 vex 3417 . . . . . . . . . . . 12 𝑏 ∈ V
159158eldm 5557 . . . . . . . . . . 11 (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
1603, 159anbi12i 620 . . . . . . . . . 10 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
161 exdistrv 2054 . . . . . . . . . 10 (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
162160, 161bitr4i 270 . . . . . . . . 9 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ ∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡))
16382simprd 491 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
164163simpld 490 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 We 𝑏)
165164ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
166 weso 5337 . . . . . . . . . . . . . . 15 (𝑡 We 𝑏𝑡 Or 𝑏)
167165, 166syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
168 simprl 787 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎𝑏)
169 simplrl 795 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑎)
170168, 169sseldd 3828 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑏)
171 simplrr 796 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
172 solin 5289 . . . . . . . . . . . . . 14 ((𝑡 Or 𝑏 ∧ (𝑦𝑏𝑤𝑏)) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
173167, 170, 171, 172syl12anc 870 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
17421relelrni 5600 . . . . . . . . . . . . . . . . . 18 (𝑏𝑊𝑡𝑡 ∈ ran 𝑊)
175174ad2antll 720 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
176175ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
177 elssuni 4691 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ran 𝑊𝑡 ran 𝑊)
178176, 177syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ran 𝑊)
179178ssbrd 4918 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 ran 𝑊 𝑤))
180 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤𝑦 = 𝑤))
181178ssbrd 4918 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦𝑤 ran 𝑊 𝑦))
182179, 180, 1813orim123d 1572 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
183173, 182mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
18449adantrr 708 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 We 𝑎)
185184ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
186 weso 5337 . . . . . . . . . . . . . . 15 (𝑠 We 𝑎𝑠 Or 𝑎)
187185, 186syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
188 simplrl 795 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦𝑎)
189 simprl 787 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
190 simplrr 796 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
191189, 190sseldd 3828 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
192 solin 5289 . . . . . . . . . . . . . 14 ((𝑠 Or 𝑎 ∧ (𝑦𝑎𝑤𝑎)) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
193187, 188, 191, 192syl12anc 870 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
19421relelrni 5600 . . . . . . . . . . . . . . . . . 18 (𝑎𝑊𝑠𝑠 ∈ ran 𝑊)
195194ad2antrl 719 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
196195ad2antrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
197 elssuni 4691 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ran 𝑊𝑠 ran 𝑊)
198196, 197syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ran 𝑊)
199198ssbrd 4918 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 ran 𝑊 𝑤))
200 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤𝑦 = 𝑤))
201198ssbrd 4918 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦𝑤 ran 𝑊 𝑦))
202199, 200, 2013orim123d 1572 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
203193, 202mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
204127adantr 474 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
205183, 203, 204mpjaodan 986 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
206205exp31 412 . . . . . . . . . 10 (𝜑 → ((𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
207206exlimdvv 2033 . . . . . . . . 9 (𝜑 → (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
208162, 207syl5bi 234 . . . . . . . 8 (𝜑 → ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
209208rexlimdvv 3247 . . . . . . 7 (𝜑 → (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
210157, 209syl5bi 234 . . . . . 6 (𝜑 → ((𝑦𝑋𝑤𝑋) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
211210ralrimivv 3179 . . . . 5 (𝜑 → ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
212 dfwe2 7247 . . . . 5 ( ran 𝑊 We 𝑋 ↔ ( ran 𝑊 Fr 𝑋 ∧ ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
213151, 211, 212sylanbrc 578 . . . 4 (𝜑 ran 𝑊 We 𝑋)
2144fpwwe2cbv 9774 . . . . . . . . . . . . 13 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧𝐴𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤𝑧 [(𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
2155adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝐴 ∈ V)
216 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎𝑊𝑠)
217214, 215, 216fpwwe2lem3 9777 . . . . . . . . . . . 12 (((𝜑𝑎𝑊𝑠) ∧ 𝑦𝑎) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
218217anasss 460 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
219 cnvimass 5730 . . . . . . . . . . . . 13 ( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊
2205, 17ssexd 5032 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ V)
221220, 220xpexd 7226 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 × 𝑋) ∈ V)
222221, 37ssexd 5032 . . . . . . . . . . . . . . 15 (𝜑 ran 𝑊 ∈ V)
223222adantr 474 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ran 𝑊 ∈ V)
224223dmexd 7365 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → dom ran 𝑊 ∈ V)
225 ssexg 5031 . . . . . . . . . . . . 13 ((( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊 ∧ dom ran 𝑊 ∈ V) → ( ran 𝑊 “ {𝑦}) ∈ V)
226219, 224, 225sylancr 581 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) ∈ V)
227 id 22 . . . . . . . . . . . . . . 15 (𝑢 = ( ran 𝑊 “ {𝑦}) → 𝑢 = ( ran 𝑊 “ {𝑦}))
228 olc 899 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
229 df-br 4876 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ran 𝑊)
230 eluni2 4664 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑧, 𝑤⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
231229, 230bitri 267 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
232 df-br 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
23384ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
234233ssbrd 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑏)𝑤))
235 brxp 5392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧𝑏𝑤𝑏))
236235simplbi 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑧(𝑏 × 𝑏)𝑤𝑧𝑏)
237234, 236syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑏))
23820adantrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
239238ssbrd 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑤𝑠𝑦𝑤(𝑎 × 𝑎)𝑦))
240239imp 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
241 brxp 5392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤𝑎𝑦𝑎))
242241simplbi 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤(𝑎 × 𝑎)𝑦𝑤𝑎)
243240, 242syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤𝑎)
244243a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦𝑎𝑤𝑎))
245 elequ1 2171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤 = 𝑦 → (𝑤𝑎𝑦𝑎))
246245biimprd 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑤 = 𝑦 → (𝑦𝑎𝑤𝑎))
247246adantl 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦𝑎𝑤𝑎))
248244, 247jaodan 985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑦𝑎𝑤𝑎))
249248impr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → 𝑤𝑎)
250249adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
251237, 250jctird 522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑏𝑤𝑎)))
252 brxp 5392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧𝑏𝑤𝑎))
253251, 252syl6ibr 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
254253ancld 546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
255 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
256255breqd 4886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
257 brin 4927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
258256, 257syl6bb 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
259254, 258sylibrd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
260 simprr 789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
261260, 118syl6eqss 3880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
262261ssbrd 4918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
263127adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
264259, 262, 263mpjaodan 986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (𝑧𝑡𝑤𝑧𝑠𝑤))
265232, 264syl5bir 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
266265exp32 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
267266expr 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
268267com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑎𝑊𝑠) → (𝑦𝑎 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
269268impr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
270269imp 397 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
271270exlimdv 2032 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
27270, 271syl5bi 234 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
273272rexlimdv 3239 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
274231, 273syl5bi 234 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
275228, 274sylan2 586 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤 = 𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
276275ex 403 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
277276alrimiv 2026 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
278 breq2 4879 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧 ran 𝑊 𝑦))
279 breq2 4879 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧𝑠𝑤𝑧𝑠𝑦))
280278, 279imbi12d 336 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → ((𝑧 ran 𝑊 𝑤𝑧𝑠𝑤) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦)))
281280equsalvw 2108 . . . . . . . . . . . . . . . . . . 19 (∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
282277, 281sylib 210 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
283194ad2antrl 719 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ∈ ran 𝑊)
284283, 197syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ran 𝑊)
285284ssbrd 4918 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧𝑠𝑦𝑧 ran 𝑊 𝑦))
286282, 285impbid 204 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
287 vex 3417 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
288287eliniseg 5739 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦))
289288elv 3418 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦)
290287eliniseg 5739 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
291290elv 3418 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
292286, 289, 2913bitr4g 306 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (𝑠 “ {𝑦})))
293292eqrdv 2823 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) = (𝑠 “ {𝑦}))
294227, 293sylan9eqr 2883 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → 𝑢 = (𝑠 “ {𝑦}))
295294sqxpeqd 5378 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
296295ineq2d 4043 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
297 relinxp 5476 . . . . . . . . . . . . . . . . 17 Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
298 relinxp 5476 . . . . . . . . . . . . . . . . 17 Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
299 vex 3417 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
300299eliniseg 5739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ V → (𝑤 ∈ (𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
301290, 300anbi12d 624 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ V → ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦)))
302301elv 3418 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦))
303 orc 898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑠𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
304303, 274sylan2 586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
305304adantrl 707 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
306284adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → 𝑠 ran 𝑊)
307306ssbrd 4918 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧𝑠𝑤𝑧 ran 𝑊 𝑤))
308305, 307impbid 204 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
309302, 308sylan2b 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}))) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
310309pm5.32da 574 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
311 df-br 4876 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
312 brinxp2 5417 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
313311, 312bitr3i 269 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
314 df-br 4876 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
315 brinxp2 5417 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
316314, 315bitr3i 269 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
317310, 313, 3163bitr4g 306 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
318297, 298, 317eqrelrdv 5454 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
319318adantr 474 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
320296, 319eqtrd 2861 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
321294, 320oveq12d 6928 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
322321eqeq1d 2827 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ((𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
323226, 322sbcied 3699 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ([( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
324218, 323mpbird 249 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
325324exp32 413 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
326325exlimdv 2032 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
3273, 326syl5bi 234 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
328327rexlimdv 3239 . . . . . 6 (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
32944, 328syl5bi 234 . . . . 5 (𝜑 → (𝑦𝑋[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
330329ralrimiv 3174 . . . 4 (𝜑 → ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
331213, 330jca 507 . . 3 (𝜑 → ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
3324, 5fpwwe2lem2 9776 . . 3 (𝜑 → (𝑋𝑊 ran 𝑊 ↔ ((𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
33338, 331, 332mpbir2and 704 . 2 (𝜑𝑋𝑊 ran 𝑊)
33421releldmi 5599 . 2 (𝑋𝑊 ran 𝑊𝑋 ∈ dom 𝑊)
335333, 334syl 17 1 (𝜑𝑋 ∈ dom 𝑊)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 878   ∨ w3o 1110   ∧ w3a 1111  ∀wal 1654   = wceq 1656  ∃wex 1878   ∈ wcel 2164   ≠ wne 2999  ∀wral 3117  ∃wrex 3118  Vcvv 3414  [wsbc 3662   ∩ cin 3797   ⊆ wss 3798  ∅c0 4146  𝒫 cpw 4380  {csn 4399  ⟨cop 4405  ∪ cuni 4660   class class class wbr 4875  {copab 4937   Or wor 5264   Fr wfr 5302   We wwe 5304   × cxp 5344  ◡ccnv 5345  dom cdm 5346  ran crn 5347   “ cima 5349  (class class class)co 6910 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-wrecs 7677  df-recs 7739  df-oi 8691 This theorem is referenced by:  fpwwe2lem13  9786  fpwwe2  9787
 Copyright terms: Public domain W3C validator