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

Theorem fpwwe2lem12 9415
Description: Lemma for fpwwe2 9417. (Contributed by Mario Carneiro, 18-May-2015.)
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 3192 . . . . . . . . 9 𝑎 ∈ V
32eldm 5286 . . . . . . . 8 (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5 fpwwe2.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ V)
64, 5fpwwe2lem2 9406 . . . . . . . . . . . . 13 (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
76simprbda 652 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)))
87simpld 475 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑎𝐴)
9 selpw 4142 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
108, 9sylibr 224 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
1110ex 450 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
1211exlimdv 1858 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
133, 12syl5bi 232 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊𝑎 ∈ 𝒫 𝐴))
1413ssrdv 3593 . . . . . 6 (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15 sspwuni 4582 . . . . . 6 (dom 𝑊 ⊆ 𝒫 𝐴 dom 𝑊𝐴)
1614, 15sylib 208 . . . . 5 (𝜑 dom 𝑊𝐴)
171, 16syl5eqss 3633 . . . 4 (𝜑𝑋𝐴)
18 vex 3192 . . . . . . . 8 𝑠 ∈ V
1918elrn 5331 . . . . . . 7 (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
207simprd 479 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
214relopabi 5210 . . . . . . . . . . . . . . . 16 Rel 𝑊
2221releldmi 5327 . . . . . . . . . . . . . . 15 (𝑎𝑊𝑠𝑎 ∈ dom 𝑊)
2322adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24 elssuni 4438 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑊𝑎 dom 𝑊)
2523, 24syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎 dom 𝑊)
2625, 1syl6sseqr 3636 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → 𝑎𝑋)
27 xpss12 5191 . . . . . . . . . . . 12 ((𝑎𝑋𝑎𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2826, 26, 27syl2anc 692 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2920, 28sstrd 3597 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30 selpw 4142 . . . . . . . . . 10 (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
3129, 30sylibr 224 . . . . . . . . 9 ((𝜑𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
3231ex 450 . . . . . . . 8 (𝜑 → (𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3332exlimdv 1858 . . . . . . 7 (𝜑 → (∃𝑎 𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3419, 33syl5bi 232 . . . . . 6 (𝜑 → (𝑠 ∈ ran 𝑊𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3534ssrdv 3593 . . . . 5 (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36 sspwuni 4582 . . . . 5 (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ran 𝑊 ⊆ (𝑋 × 𝑋))
3735, 36sylib 208 . . . 4 (𝜑 ran 𝑊 ⊆ (𝑋 × 𝑋))
3817, 37jca 554 . . 3 (𝜑 → (𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)))
39 n0 3912 . . . . . . . . 9 (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦𝑛)
40 ssel2 3582 . . . . . . . . . . . . . 14 ((𝑛𝑋𝑦𝑛) → 𝑦𝑋)
4140adantl 482 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → 𝑦𝑋)
421eleq2i 2690 . . . . . . . . . . . . . 14 (𝑦𝑋𝑦 dom 𝑊)
43 eluni2 4411 . . . . . . . . . . . . . 14 (𝑦 dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4442, 43bitri 264 . . . . . . . . . . . . 13 (𝑦𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4541, 44sylib 208 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
462inex2 4765 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ∈ V
4746a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ∈ V)
486simplbda 653 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
4948simpld 475 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎𝑊𝑠) → 𝑠 We 𝑎)
5049ad2ant2r 782 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 We 𝑎)
51 wefr 5069 . . . . . . . . . . . . . . . . . . 19 (𝑠 We 𝑎𝑠 Fr 𝑎)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 Fr 𝑎)
53 inss2 3817 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ⊆ 𝑎
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ⊆ 𝑎)
55 simplrr 800 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑛)
56 simprr 795 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑎)
57 inelcm 4009 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑛𝑦𝑎) → (𝑛𝑎) ≠ ∅)
5855, 56, 57syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ≠ ∅)
59 fri 5041 . . . . . . . . . . . . . . . . . 18 ((((𝑛𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛𝑎) ⊆ 𝑎 ∧ (𝑛𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
6047, 52, 54, 58, 59syl22anc 1324 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
61 inss1 3816 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑎) ⊆ 𝑛
62 simprl 793 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛𝑎))
6361, 62sseldi 3585 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑛)
64 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
65 ralnex 2987 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
6664, 65sylib 208 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
67 df-br 4619 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ran 𝑊)
68 eluni2 4411 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑤, 𝑣⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
6967, 68bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
70 vex 3192 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ∈ V
7170elrn 5331 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
72 df-br 4619 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
73 simprll 801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑛)
7473adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑛)
75 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
76 simp-4l 805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
77 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑎𝑊𝑠)
7877ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
79 simprlr 802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
80 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
814, 5fpwwe2lem2 9406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8281adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8380, 82mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
8483simpld 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)))
8584simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
8676, 78, 79, 85syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
8786ssbrd 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣𝑤(𝑏 × 𝑏)𝑣))
8875, 87mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
89 brxp 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤𝑏𝑣𝑏))
9089simplbi 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑤(𝑏 × 𝑏)𝑣𝑤𝑏)
9188, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑏)
9291adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
9353, 62sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑎)
9493ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣𝑎)
95 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
96 brinxp2 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ (𝑤𝑏𝑣𝑎𝑤𝑡𝑣))
9792, 94, 95, 96syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
98 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
9998breqd 4629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
10097, 99mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
10176, 78, 20syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
102101adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
103102ssbrd 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑎 × 𝑎)𝑣))
104100, 103mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
105 brxp 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤𝑎𝑣𝑎))
106105simplbi 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤(𝑎 × 𝑎)𝑣𝑤𝑎)
107104, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
10874, 107elind 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛𝑎))
109 breq1 4621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑤 → (𝑧𝑠𝑣𝑤𝑠𝑣))
110109rspcev 3298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑤 ∈ (𝑛𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
111108, 100, 110syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
11273adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑛)
113 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
11491adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
115113, 114sseldd 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
116112, 115elind 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛𝑎))
117 simplrr 800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
118 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
119 inss1 3816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
120118, 119syl6eqss 3639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
121120ssbrd 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣𝑤𝑠𝑣))
122117, 121mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
123116, 122, 110syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
1245adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝐴 ∈ V)
125 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126125adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
127 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
1284, 124, 126, 127, 80fpwwe2lem10 9413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
12976, 78, 79, 128syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
130111, 123, 129mpjaodan 826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
131130expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13272, 131syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
133132expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
134133exlimdv 1858 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
13571, 134syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
136135rexlimdv 3024 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13769, 136syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑤 ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13866, 137mtod 189 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ 𝑤 ran 𝑊 𝑣)
139138ralrimiva 2961 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
14063, 139jca 554 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → (𝑣𝑛 ∧ ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
141140ex 450 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣) → (𝑣𝑛 ∧ ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
142141reximdv2 3009 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14360, 142mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
144143exp32 630 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
145144exlimdv 1858 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
1463, 145syl5bi 232 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
147146rexlimdv 3024 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14845, 147mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
149148expr 642 . . . . . . . . . 10 ((𝜑𝑛𝑋) → (𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
150149exlimdv 1858 . . . . . . . . 9 ((𝜑𝑛𝑋) → (∃𝑦 𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
15139, 150syl5bi 232 . . . . . . . 8 ((𝜑𝑛𝑋) → (𝑛 ≠ ∅ → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
152151expimpd 628 . . . . . . 7 (𝜑 → ((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
153152alrimiv 1852 . . . . . 6 (𝜑 → ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
154 df-fr 5038 . . . . . 6 ( ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
155153, 154sylibr 224 . . . . 5 (𝜑 ran 𝑊 Fr 𝑋)
1561eleq2i 2690 . . . . . . . . . 10 (𝑤𝑋𝑤 dom 𝑊)
157 eluni2 4411 . . . . . . . . . 10 (𝑤 dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
158156, 157bitri 264 . . . . . . . . 9 (𝑤𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
15944, 158anbi12i 732 . . . . . . . 8 ((𝑦𝑋𝑤𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
160 reeanv 3100 . . . . . . . 8 (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
161159, 160bitr4i 267 . . . . . . 7 ((𝑦𝑋𝑤𝑋) ↔ ∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏))
162 vex 3192 . . . . . . . . . . . 12 𝑏 ∈ V
163162eldm 5286 . . . . . . . . . . 11 (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
1643, 163anbi12i 732 . . . . . . . . . 10 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
165 eeanv 2181 . . . . . . . . . 10 (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
166164, 165bitr4i 267 . . . . . . . . 9 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ ∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡))
16783simprd 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
168167simpld 475 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 We 𝑏)
169168ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
170 weso 5070 . . . . . . . . . . . . . . 15 (𝑡 We 𝑏𝑡 Or 𝑏)
171169, 170syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
172 simprl 793 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎𝑏)
173 simplrl 799 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑎)
174172, 173sseldd 3588 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑏)
175 simplrr 800 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
176 solin 5023 . . . . . . . . . . . . . 14 ((𝑡 Or 𝑏 ∧ (𝑦𝑏𝑤𝑏)) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
177171, 174, 175, 176syl12anc 1321 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
17821relelrni 5328 . . . . . . . . . . . . . . . . . 18 (𝑏𝑊𝑡𝑡 ∈ ran 𝑊)
179178ad2antll 764 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
180179ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
181 elssuni 4438 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ran 𝑊𝑡 ran 𝑊)
182180, 181syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ran 𝑊)
183182ssbrd 4661 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 ran 𝑊 𝑤))
184 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤𝑦 = 𝑤))
185182ssbrd 4661 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦𝑤 ran 𝑊 𝑦))
186183, 184, 1853orim123d 1404 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
187177, 186mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
18849adantrr 752 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 We 𝑎)
189188ad2antrr 761 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
190 weso 5070 . . . . . . . . . . . . . . 15 (𝑠 We 𝑎𝑠 Or 𝑎)
191189, 190syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
192 simplrl 799 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦𝑎)
193 simprl 793 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
194 simplrr 800 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
195193, 194sseldd 3588 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
196 solin 5023 . . . . . . . . . . . . . 14 ((𝑠 Or 𝑎 ∧ (𝑦𝑎𝑤𝑎)) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
197191, 192, 195, 196syl12anc 1321 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
19821relelrni 5328 . . . . . . . . . . . . . . . . . 18 (𝑎𝑊𝑠𝑠 ∈ ran 𝑊)
199198ad2antrl 763 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
200199ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
201 elssuni 4438 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ran 𝑊𝑠 ran 𝑊)
202200, 201syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ran 𝑊)
203202ssbrd 4661 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 ran 𝑊 𝑤))
204 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤𝑦 = 𝑤))
205202ssbrd 4661 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦𝑤 ran 𝑊 𝑦))
206203, 204, 2053orim123d 1404 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
207197, 206mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
208128adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
209187, 207, 208mpjaodan 826 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
210209exp31 629 . . . . . . . . . 10 (𝜑 → ((𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
211210exlimdvv 1859 . . . . . . . . 9 (𝜑 → (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
212166, 211syl5bi 232 . . . . . . . 8 (𝜑 → ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
213212rexlimdvv 3031 . . . . . . 7 (𝜑 → (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
214161, 213syl5bi 232 . . . . . 6 (𝜑 → ((𝑦𝑋𝑤𝑋) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
215214ralrimivv 2965 . . . . 5 (𝜑 → ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
216 dfwe2 6935 . . . . 5 ( ran 𝑊 We 𝑋 ↔ ( ran 𝑊 Fr 𝑋 ∧ ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
217155, 215, 216sylanbrc 697 . . . 4 (𝜑 ran 𝑊 We 𝑋)
2184fpwwe2cbv 9404 . . . . . . . . . . . . 13 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧𝐴𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤𝑧 [(𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
2195adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝐴 ∈ V)
220 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎𝑊𝑠)
221218, 219, 220fpwwe2lem3 9407 . . . . . . . . . . . 12 (((𝜑𝑎𝑊𝑠) ∧ 𝑦𝑎) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
222221anasss 678 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
223 cnvimass 5449 . . . . . . . . . . . . 13 ( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊
2245, 17ssexd 4770 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ V)
225 xpexg 6920 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V)
226224, 224, 225syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 × 𝑋) ∈ V)
227226, 37ssexd 4770 . . . . . . . . . . . . . . 15 (𝜑 ran 𝑊 ∈ V)
228227adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ran 𝑊 ∈ V)
229 dmexg 7051 . . . . . . . . . . . . . 14 ( ran 𝑊 ∈ V → dom ran 𝑊 ∈ V)
230228, 229syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → dom ran 𝑊 ∈ V)
231 ssexg 4769 . . . . . . . . . . . . 13 ((( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊 ∧ dom ran 𝑊 ∈ V) → ( ran 𝑊 “ {𝑦}) ∈ V)
232223, 230, 231sylancr 694 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) ∈ V)
233 id 22 . . . . . . . . . . . . . . 15 (𝑢 = ( ran 𝑊 “ {𝑦}) → 𝑢 = ( ran 𝑊 “ {𝑦}))
234 olc 399 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
235 df-br 4619 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ran 𝑊)
236 eluni2 4411 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑧, 𝑤⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
237235, 236bitri 264 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
238 df-br 4619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
23985ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
240239ssbrd 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑏)𝑤))
241 brxp 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧𝑏𝑤𝑏))
242241simplbi 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑧(𝑏 × 𝑏)𝑤𝑧𝑏)
243240, 242syl6 35 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑏))
24420adantrr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
245244ssbrd 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑤𝑠𝑦𝑤(𝑎 × 𝑎)𝑦))
246245imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
247 brxp 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤𝑎𝑦𝑎))
248247simplbi 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤(𝑎 × 𝑎)𝑦𝑤𝑎)
249246, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤𝑎)
250249a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦𝑎𝑤𝑎))
251 elequ1 1994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤 = 𝑦 → (𝑤𝑎𝑦𝑎))
252251biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑤 = 𝑦 → (𝑦𝑎𝑤𝑎))
253252adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦𝑎𝑤𝑎))
254250, 253jaodan 825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑦𝑎𝑤𝑎))
255254impr 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → 𝑤𝑎)
256255adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
257243, 256jctird 566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑏𝑤𝑎)))
258 brxp 5112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧𝑏𝑤𝑎))
259257, 258syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
260259ancld 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
261 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
262261breqd 4629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
263 brin 4669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
264262, 263syl6bb 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
265260, 264sylibrd 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
266 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
267266, 119syl6eqss 3639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
268267ssbrd 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
269128adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
270265, 268, 269mpjaodan 826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (𝑧𝑡𝑤𝑧𝑠𝑤))
271238, 270syl5bir 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
272271exp32 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
273272expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
274273com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑎𝑊𝑠) → (𝑦𝑎 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
275274impr 648 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
276275imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
277276exlimdv 1858 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
27871, 277syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
279278rexlimdv 3024 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
280237, 279syl5bi 232 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
281234, 280sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤 = 𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
282281ex 450 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
283282alrimiv 1852 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
284 vex 3192 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
285 breq2 4622 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧 ran 𝑊 𝑦))
286 breq2 4622 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧𝑠𝑤𝑧𝑠𝑦))
287285, 286imbi12d 334 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → ((𝑧 ran 𝑊 𝑤𝑧𝑠𝑤) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦)))
288284, 287ceqsalv 3222 . . . . . . . . . . . . . . . . . . 19 (∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
289283, 288sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
290198ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ∈ ran 𝑊)
291290, 201syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ran 𝑊)
292291ssbrd 4661 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧𝑠𝑦𝑧 ran 𝑊 𝑦))
293289, 292impbid 202 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
294 vex 3192 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
295294eliniseg 5458 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦))
296284, 295ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦)
297294eliniseg 5458 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
298284, 297ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
299293, 296, 2983bitr4g 303 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (𝑠 “ {𝑦})))
300299eqrdv 2619 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) = (𝑠 “ {𝑦}))
301233, 300sylan9eqr 2677 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → 𝑢 = (𝑠 “ {𝑦}))
302301sqxpeqd 5106 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
303302ineq2d 3797 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
304 inss2 3817 . . . . . . . . . . . . . . . . . 18 ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))
305 relxp 5193 . . . . . . . . . . . . . . . . . 18 Rel ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))
306 relss 5172 . . . . . . . . . . . . . . . . . 18 (( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → (Rel ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
307304, 305, 306mp2 9 . . . . . . . . . . . . . . . . 17 Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
308 inss2 3817 . . . . . . . . . . . . . . . . . 18 (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))
309 relss 5172 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → (Rel ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
310308, 305, 309mp2 9 . . . . . . . . . . . . . . . . 17 Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
311 vex 3192 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
312311eliniseg 5458 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ V → (𝑤 ∈ (𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
313297, 312anbi12d 746 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ V → ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦)))
314284, 313ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦))
315 orc 400 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑠𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
316315, 280sylan2 491 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
317316adantrl 751 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
318291adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → 𝑠 ran 𝑊)
319318ssbrd 4661 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧𝑠𝑤𝑧 ran 𝑊 𝑤))
320317, 319impbid 202 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
321314, 320sylan2b 492 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}))) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
322321pm5.32da 672 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
323 brinxp2 5146 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧 ran 𝑊 𝑤))
324 df-br 4619 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
325 df-3an 1038 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
326323, 324, 3253bitr3i 290 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
327 brinxp2 5146 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧𝑠𝑤))
328 df-br 4619 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
329 df-3an 1038 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧𝑠𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
330327, 328, 3293bitr3i 290 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
331322, 326, 3303bitr4g 303 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
332307, 310, 331eqrelrdv 5182 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
333332adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
334303, 333eqtrd 2655 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
335301, 334oveq12d 6628 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
336335eqeq1d 2623 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ((𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
337232, 336sbcied 3458 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ([( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
338222, 337mpbird 247 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
339338exp32 630 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
340339exlimdv 1858 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
3413, 340syl5bi 232 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
342341rexlimdv 3024 . . . . . 6 (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
34344, 342syl5bi 232 . . . . 5 (𝜑 → (𝑦𝑋[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
344343ralrimiv 2960 . . . 4 (𝜑 → ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
345217, 344jca 554 . . 3 (𝜑 → ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
3464, 5fpwwe2lem2 9406 . . 3 (𝜑 → (𝑋𝑊 ran 𝑊 ↔ ((𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
34738, 345, 346mpbir2and 956 . 2 (𝜑𝑋𝑊 ran 𝑊)
34821releldmi 5327 . 2 (𝑋𝑊 ran 𝑊𝑋 ∈ dom 𝑊)
349347, 348syl 17 1 (𝜑𝑋 ∈ dom 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035  w3a 1036  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3189  [wsbc 3421  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153  cop 4159   cuni 4407   class class class wbr 4618  {copab 4677   Or wor 4999   Fr wfr 5035   We wwe 5037   × cxp 5077  ccnv 5078  dom cdm 5079  ran crn 5080  cima 5082  Rel wrel 5084  (class class class)co 6610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-wrecs 7359  df-recs 7420  df-oi 8367
This theorem is referenced by:  fpwwe2lem13  9416  fpwwe2  9417
  Copyright terms: Public domain W3C validator