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

Theorem fpwwe2lem12 9342
Description: Lemma for fpwwe2 9344. (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 3176 . . . . . . . . 9 𝑎 ∈ V
32eldm 5243 . . . . . . . 8 (𝑎 ∈ dom 𝑊 ↔ ∃𝑠 𝑎𝑊𝑠)
4 fpwwe2.1 . . . . . . . . . . . . . 14 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
5 fpwwe2.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ V)
64, 5fpwwe2lem2 9333 . . . . . . . . . . . . 13 (𝜑 → (𝑎𝑊𝑠 ↔ ((𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))))
76simprbda 651 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → (𝑎𝐴𝑠 ⊆ (𝑎 × 𝑎)))
87simpld 474 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑎𝐴)
9 selpw 4115 . . . . . . . . . . 11 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
108, 9sylibr 223 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ 𝒫 𝐴)
1110ex 449 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
1211exlimdv 1848 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠𝑎 ∈ 𝒫 𝐴))
133, 12syl5bi 231 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊𝑎 ∈ 𝒫 𝐴))
1413ssrdv 3574 . . . . . 6 (𝜑 → dom 𝑊 ⊆ 𝒫 𝐴)
15 sspwuni 4547 . . . . . 6 (dom 𝑊 ⊆ 𝒫 𝐴 dom 𝑊𝐴)
1614, 15sylib 207 . . . . 5 (𝜑 dom 𝑊𝐴)
171, 16syl5eqss 3612 . . . 4 (𝜑𝑋𝐴)
18 vex 3176 . . . . . . . 8 𝑠 ∈ V
1918elrn 5287 . . . . . . 7 (𝑠 ∈ ran 𝑊 ↔ ∃𝑎 𝑎𝑊𝑠)
207simprd 478 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑎 × 𝑎))
214relopabi 5167 . . . . . . . . . . . . . . . 16 Rel 𝑊
2221releldmi 5283 . . . . . . . . . . . . . . 15 (𝑎𝑊𝑠𝑎 ∈ dom 𝑊)
2322adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑊𝑠) → 𝑎 ∈ dom 𝑊)
24 elssuni 4403 . . . . . . . . . . . . . 14 (𝑎 ∈ dom 𝑊𝑎 dom 𝑊)
2523, 24syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎 dom 𝑊)
2625, 1syl6sseqr 3615 . . . . . . . . . . . 12 ((𝜑𝑎𝑊𝑠) → 𝑎𝑋)
27 xpss12 5148 . . . . . . . . . . . 12 ((𝑎𝑋𝑎𝑋) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2826, 26, 27syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑎𝑊𝑠) → (𝑎 × 𝑎) ⊆ (𝑋 × 𝑋))
2920, 28sstrd 3578 . . . . . . . . . 10 ((𝜑𝑎𝑊𝑠) → 𝑠 ⊆ (𝑋 × 𝑋))
30 selpw 4115 . . . . . . . . . 10 (𝑠 ∈ 𝒫 (𝑋 × 𝑋) ↔ 𝑠 ⊆ (𝑋 × 𝑋))
3129, 30sylibr 223 . . . . . . . . 9 ((𝜑𝑎𝑊𝑠) → 𝑠 ∈ 𝒫 (𝑋 × 𝑋))
3231ex 449 . . . . . . . 8 (𝜑 → (𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3332exlimdv 1848 . . . . . . 7 (𝜑 → (∃𝑎 𝑎𝑊𝑠𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3419, 33syl5bi 231 . . . . . 6 (𝜑 → (𝑠 ∈ ran 𝑊𝑠 ∈ 𝒫 (𝑋 × 𝑋)))
3534ssrdv 3574 . . . . 5 (𝜑 → ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋))
36 sspwuni 4547 . . . . 5 (ran 𝑊 ⊆ 𝒫 (𝑋 × 𝑋) ↔ ran 𝑊 ⊆ (𝑋 × 𝑋))
3735, 36sylib 207 . . . 4 (𝜑 ran 𝑊 ⊆ (𝑋 × 𝑋))
3817, 37jca 553 . . 3 (𝜑 → (𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)))
39 n0 3890 . . . . . . . . 9 (𝑛 ≠ ∅ ↔ ∃𝑦 𝑦𝑛)
40 ssel2 3563 . . . . . . . . . . . . . 14 ((𝑛𝑋𝑦𝑛) → 𝑦𝑋)
4140adantl 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → 𝑦𝑋)
421eleq2i 2680 . . . . . . . . . . . . . 14 (𝑦𝑋𝑦 dom 𝑊)
43 eluni2 4376 . . . . . . . . . . . . . 14 (𝑦 dom 𝑊 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4442, 43bitri 263 . . . . . . . . . . . . 13 (𝑦𝑋 ↔ ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
4541, 44sylib 207 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑎 ∈ dom 𝑊 𝑦𝑎)
462inex2 4728 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ∈ V
4746a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ∈ V)
486simplbda 652 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎𝑊𝑠) → (𝑠 We 𝑎 ∧ ∀𝑦𝑎 [(𝑠 “ {𝑦}) / 𝑢](𝑢𝐹(𝑠 ∩ (𝑢 × 𝑢))) = 𝑦))
4948simpld 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑎𝑊𝑠) → 𝑠 We 𝑎)
5049ad2ant2r 779 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 We 𝑎)
51 wefr 5028 . . . . . . . . . . . . . . . . . . 19 (𝑠 We 𝑎𝑠 Fr 𝑎)
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 Fr 𝑎)
53 inss2 3796 . . . . . . . . . . . . . . . . . . 19 (𝑛𝑎) ⊆ 𝑎
5453a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ⊆ 𝑎)
55 simplrr 797 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑛)
56 simprr 792 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑦𝑎)
57 inelcm 3984 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑛𝑦𝑎) → (𝑛𝑎) ≠ ∅)
5855, 56, 57syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑛𝑎) ≠ ∅)
59 fri 5000 . . . . . . . . . . . . . . . . . 18 ((((𝑛𝑎) ∈ V ∧ 𝑠 Fr 𝑎) ∧ ((𝑛𝑎) ⊆ 𝑎 ∧ (𝑛𝑎) ≠ ∅)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
6047, 52, 54, 58, 59syl22anc 1319 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
61 inss1 3795 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑎) ⊆ 𝑛
62 simprl 790 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣 ∈ (𝑛𝑎))
6361, 62sseldi 3566 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑛)
64 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)
65 ralnex 2975 . . . . . . . . . . . . . . . . . . . . . . 23 (∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 ↔ ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
6664, 65sylib 207 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
67 df-br 4584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ran 𝑊 𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ ran 𝑊)
68 eluni2 4376 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑤, 𝑣⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
6967, 68bitri 263 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ran 𝑊 𝑣 ↔ ∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡)
70 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ∈ V
7170elrn 5287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ ran 𝑊 ↔ ∃𝑏 𝑏𝑊𝑡)
72 df-br 4584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤𝑡𝑣 ↔ ⟨𝑤, 𝑣⟩ ∈ 𝑡)
73 simprll 798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑛)
7473adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑛)
75 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑡𝑣)
76 simp-4l 802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝜑)
77 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑎𝑊𝑠)
7877ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑎𝑊𝑠)
79 simprlr 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑏𝑊𝑡)
80 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑏𝑊𝑡)
814, 5fpwwe2lem2 9333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8281adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝑊𝑡 ↔ ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))))
8380, 82mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)) ∧ (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦)))
8483simpld 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑏𝐴𝑡 ⊆ (𝑏 × 𝑏)))
8584simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ⊆ (𝑏 × 𝑏))
8676, 78, 79, 85syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑡 ⊆ (𝑏 × 𝑏))
8786ssbrd 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → (𝑤𝑡𝑣𝑤(𝑏 × 𝑏)𝑣))
8875, 87mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤(𝑏 × 𝑏)𝑣)
89 brxp 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑤(𝑏 × 𝑏)𝑣 ↔ (𝑤𝑏𝑣𝑏))
9089simplbi 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑤(𝑏 × 𝑏)𝑣𝑤𝑏)
9188, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑤𝑏)
9291adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
9353, 62sseldi 3566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → 𝑣𝑎)
9493ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑣𝑎)
95 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑡𝑣)
96 brinxp2 5103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣 ↔ (𝑤𝑏𝑣𝑎𝑤𝑡𝑣))
9792, 94, 95, 96syl3anbrc 1239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣)
98 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
9998breqd 4594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑡 ∩ (𝑏 × 𝑎))𝑣))
10097, 99mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑠𝑣)
10176, 78, 20syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → 𝑠 ⊆ (𝑎 × 𝑎))
102101adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 ⊆ (𝑎 × 𝑎))
103102ssbrd 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑠𝑣𝑤(𝑎 × 𝑎)𝑣))
104100, 103mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤(𝑎 × 𝑎)𝑣)
105 brxp 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑤(𝑎 × 𝑎)𝑣 ↔ (𝑤𝑎𝑣𝑎))
106105simplbi 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑤(𝑎 × 𝑎)𝑣𝑤𝑎)
107104, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
10874, 107elind 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤 ∈ (𝑛𝑎))
109 breq1 4586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧 = 𝑤 → (𝑧𝑠𝑣𝑤𝑠𝑣))
110109rspcev 3282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑤 ∈ (𝑛𝑎) ∧ 𝑤𝑠𝑣) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
111108, 100, 110syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
11273adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑛)
113 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
11491adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
115113, 114sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
116112, 115elind 3760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤 ∈ (𝑛𝑎))
117 simplrr 797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑡𝑣)
118 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
119 inss1 3795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑠 ∩ (𝑎 × 𝑏)) ⊆ 𝑠
120118, 119syl6eqss 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
121120ssbrd 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑡𝑣𝑤𝑠𝑣))
122117, 121mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑠𝑣)
123116, 122, 110syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
1245adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝐴 ∈ V)
125 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
126125adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
127 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑎𝑊𝑠)
1284, 124, 126, 127, 80fpwwe2lem10 9340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
12976, 78, 79, 128syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
130111, 123, 129mpjaodan 823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ ((𝑤𝑛𝑏𝑊𝑡) ∧ 𝑤𝑡𝑣)) → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)
131130expr 641 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (𝑤𝑡𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13272, 131syl5bir 232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ (𝑤𝑛𝑏𝑊𝑡)) → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
133132expr 641 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
134133exlimdv 1848 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
13571, 134syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑡 ∈ ran 𝑊 → (⟨𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣)))
136135rexlimdv 3012 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (∃𝑡 ∈ ran 𝑊𝑤, 𝑣⟩ ∈ 𝑡 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13769, 136syl5bi 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → (𝑤 ran 𝑊 𝑣 → ∃𝑧 ∈ (𝑛𝑎)𝑧𝑠𝑣))
13866, 137mtod 188 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) ∧ 𝑤𝑛) → ¬ 𝑤 ran 𝑊 𝑣)
139138ralrimiva 2949 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
14063, 139jca 553 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣)) → (𝑣𝑛 ∧ ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
141140ex 449 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑣 ∈ (𝑛𝑎) ∧ ∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣) → (𝑣𝑛 ∧ ∀𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
142141reximdv2 2997 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → (∃𝑣 ∈ (𝑛𝑎)∀𝑧 ∈ (𝑛𝑎) ¬ 𝑧𝑠𝑣 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14360, 142mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑛𝑋𝑦𝑛)) ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
144143exp32 629 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
145144exlimdv 1848 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
1463, 145syl5bi 231 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (𝑎 ∈ dom 𝑊 → (𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)))
147146rexlimdv 3012 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → (∃𝑎 ∈ dom 𝑊 𝑦𝑎 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
14845, 147mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛𝑋𝑦𝑛)) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣)
149148expr 641 . . . . . . . . . 10 ((𝜑𝑛𝑋) → (𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
150149exlimdv 1848 . . . . . . . . 9 ((𝜑𝑛𝑋) → (∃𝑦 𝑦𝑛 → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
15139, 150syl5bi 231 . . . . . . . 8 ((𝜑𝑛𝑋) → (𝑛 ≠ ∅ → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
152151expimpd 627 . . . . . . 7 (𝜑 → ((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
153152alrimiv 1842 . . . . . 6 (𝜑 → ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
154 df-fr 4997 . . . . . 6 ( ran 𝑊 Fr 𝑋 ↔ ∀𝑛((𝑛𝑋𝑛 ≠ ∅) → ∃𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣))
155153, 154sylibr 223 . . . . 5 (𝜑 ran 𝑊 Fr 𝑋)
1561eleq2i 2680 . . . . . . . . . 10 (𝑤𝑋𝑤 dom 𝑊)
157 eluni2 4376 . . . . . . . . . 10 (𝑤 dom 𝑊 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
158156, 157bitri 263 . . . . . . . . 9 (𝑤𝑋 ↔ ∃𝑏 ∈ dom 𝑊 𝑤𝑏)
15944, 158anbi12i 729 . . . . . . . 8 ((𝑦𝑋𝑤𝑋) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
160 reeanv 3086 . . . . . . . 8 (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) ↔ (∃𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃𝑏 ∈ dom 𝑊 𝑤𝑏))
161159, 160bitr4i 266 . . . . . . 7 ((𝑦𝑋𝑤𝑋) ↔ ∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏))
162 vex 3176 . . . . . . . . . . . 12 𝑏 ∈ V
163162eldm 5243 . . . . . . . . . . 11 (𝑏 ∈ dom 𝑊 ↔ ∃𝑡 𝑏𝑊𝑡)
1643, 163anbi12i 729 . . . . . . . . . 10 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
165 eeanv 2170 . . . . . . . . . 10 (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) ↔ (∃𝑠 𝑎𝑊𝑠 ∧ ∃𝑡 𝑏𝑊𝑡))
166164, 165bitr4i 266 . . . . . . . . 9 ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) ↔ ∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡))
16783simprd 478 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑡 We 𝑏 ∧ ∀𝑦𝑏 [(𝑡 “ {𝑦}) / 𝑢](𝑢𝐹(𝑡 ∩ (𝑢 × 𝑢))) = 𝑦))
168167simpld 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 We 𝑏)
169168ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 We 𝑏)
170 weso 5029 . . . . . . . . . . . . . . 15 (𝑡 We 𝑏𝑡 Or 𝑏)
171169, 170syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 Or 𝑏)
172 simprl 790 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑎𝑏)
173 simplrl 796 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑎)
174172, 173sseldd 3569 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑦𝑏)
175 simplrr 797 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑏)
176 solin 4982 . . . . . . . . . . . . . 14 ((𝑡 Or 𝑏 ∧ (𝑦𝑏𝑤𝑏)) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
177171, 174, 175, 176syl12anc 1316 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦))
17821relelrni 5284 . . . . . . . . . . . . . . . . . 18 (𝑏𝑊𝑡𝑡 ∈ ran 𝑊)
179178ad2antll 761 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑡 ∈ ran 𝑊)
180179ad2antrr 758 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ∈ ran 𝑊)
181 elssuni 4403 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ran 𝑊𝑡 ran 𝑊)
182180, 181syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ran 𝑊)
183182ssbrd 4626 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦𝑡𝑤𝑦 ran 𝑊 𝑤))
184 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 = 𝑤𝑦 = 𝑤))
185182ssbrd 4626 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑤𝑡𝑦𝑤 ran 𝑊 𝑦))
186183, 184, 1853orim123d 1399 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → ((𝑦𝑡𝑤𝑦 = 𝑤𝑤𝑡𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
187177, 186mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
18849adantrr 749 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 We 𝑎)
189188ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 We 𝑎)
190 weso 5029 . . . . . . . . . . . . . . 15 (𝑠 We 𝑎𝑠 Or 𝑎)
191189, 190syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 Or 𝑎)
192 simplrl 796 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑦𝑎)
193 simprl 790 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑏𝑎)
194 simplrr 797 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑏)
195193, 194sseldd 3569 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑤𝑎)
196 solin 4982 . . . . . . . . . . . . . 14 ((𝑠 Or 𝑎 ∧ (𝑦𝑎𝑤𝑎)) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
197191, 192, 195, 196syl12anc 1316 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦))
19821relelrni 5284 . . . . . . . . . . . . . . . . . 18 (𝑎𝑊𝑠𝑠 ∈ ran 𝑊)
199198ad2antrl 760 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ∈ ran 𝑊)
200199ad2antrr 758 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ∈ ran 𝑊)
201 elssuni 4403 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ran 𝑊𝑠 ran 𝑊)
202200, 201syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑠 ran 𝑊)
203202ssbrd 4626 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦𝑠𝑤𝑦 ran 𝑊 𝑤))
204 idd 24 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 = 𝑤𝑦 = 𝑤))
205202ssbrd 4626 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑤𝑠𝑦𝑤 ran 𝑊 𝑦))
206203, 204, 2053orim123d 1399 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → ((𝑦𝑠𝑤𝑦 = 𝑤𝑤𝑠𝑦) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
207197, 206mpd 15 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
208128adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
209187, 207, 208mpjaodan 823 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑦𝑎𝑤𝑏)) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
210209exp31 628 . . . . . . . . . 10 (𝜑 → ((𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
211210exlimdvv 1849 . . . . . . . . 9 (𝜑 → (∃𝑠𝑡(𝑎𝑊𝑠𝑏𝑊𝑡) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
212166, 211syl5bi 231 . . . . . . . 8 (𝜑 → ((𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊) → ((𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))))
213212rexlimdvv 3019 . . . . . . 7 (𝜑 → (∃𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊(𝑦𝑎𝑤𝑏) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
214161, 213syl5bi 231 . . . . . 6 (𝜑 → ((𝑦𝑋𝑤𝑋) → (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
215214ralrimivv 2953 . . . . 5 (𝜑 → ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦))
216 dfwe2 6873 . . . . 5 ( ran 𝑊 We 𝑋 ↔ ( ran 𝑊 Fr 𝑋 ∧ ∀𝑦𝑋𝑤𝑋 (𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦)))
217155, 215, 216sylanbrc 695 . . . 4 (𝜑 ran 𝑊 We 𝑋)
2184fpwwe2cbv 9331 . . . . . . . . . . . . 13 𝑊 = {⟨𝑧, 𝑡⟩ ∣ ((𝑧𝐴𝑡 ⊆ (𝑧 × 𝑧)) ∧ (𝑡 We 𝑧 ∧ ∀𝑤𝑧 [(𝑡 “ {𝑤}) / 𝑏](𝑏𝐹(𝑡 ∩ (𝑏 × 𝑏))) = 𝑤))}
2195adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝐴 ∈ V)
220 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑎𝑊𝑠) → 𝑎𝑊𝑠)
221218, 219, 220fpwwe2lem3 9334 . . . . . . . . . . . 12 (((𝜑𝑎𝑊𝑠) ∧ 𝑦𝑎) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
222221anasss 677 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦)
223 cnvimass 5404 . . . . . . . . . . . . 13 ( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊
2245, 17ssexd 4733 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ V)
225 xpexg 6858 . . . . . . . . . . . . . . . . 17 ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V)
226224, 224, 225syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋 × 𝑋) ∈ V)
227226, 37ssexd 4733 . . . . . . . . . . . . . . 15 (𝜑 ran 𝑊 ∈ V)
228227adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ran 𝑊 ∈ V)
229 dmexg 6989 . . . . . . . . . . . . . 14 ( ran 𝑊 ∈ V → dom ran 𝑊 ∈ V)
230228, 229syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → dom ran 𝑊 ∈ V)
231 ssexg 4732 . . . . . . . . . . . . 13 ((( ran 𝑊 “ {𝑦}) ⊆ dom ran 𝑊 ∧ dom ran 𝑊 ∈ V) → ( ran 𝑊 “ {𝑦}) ∈ V)
232223, 230, 231sylancr 694 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) ∈ V)
233 id 22 . . . . . . . . . . . . . . 15 (𝑢 = ( ran 𝑊 “ {𝑦}) → 𝑢 = ( ran 𝑊 “ {𝑦}))
234 olc 398 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
235 df-br 4584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ran 𝑊 𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ran 𝑊)
236 eluni2 4376 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑧, 𝑤⟩ ∈ ran 𝑊 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
237235, 236bitri 263 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 ran 𝑊 𝑤 ↔ ∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡)
238 df-br 4584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑧𝑡𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ 𝑡)
23985ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑡 ⊆ (𝑏 × 𝑏))
240239ssbrd 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑏)𝑤))
241 brxp 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑧(𝑏 × 𝑏)𝑤 ↔ (𝑧𝑏𝑤𝑏))
242241simplbi 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑧(𝑏 × 𝑏)𝑤𝑧𝑏)
243240, 242syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑏))
24420adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → 𝑠 ⊆ (𝑎 × 𝑎))
245244ssbrd 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → (𝑤𝑠𝑦𝑤(𝑎 × 𝑎)𝑦))
246245imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤(𝑎 × 𝑎)𝑦)
247 brxp 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑤(𝑎 × 𝑎)𝑦 ↔ (𝑤𝑎𝑦𝑎))
248247simplbi 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤(𝑎 × 𝑎)𝑦𝑤𝑎)
249246, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → 𝑤𝑎)
250249a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤𝑠𝑦) → (𝑦𝑎𝑤𝑎))
251 elequ1 1984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑤 = 𝑦 → (𝑤𝑎𝑦𝑎))
252251biimprd 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑤 = 𝑦 → (𝑦𝑎𝑤𝑎))
253252adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ 𝑤 = 𝑦) → (𝑦𝑎𝑤𝑎))
254250, 253jaodan 822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑦𝑎𝑤𝑎))
255254impr 647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → 𝑤𝑎)
256255adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑤𝑎)
257243, 256jctird 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑏𝑤𝑎)))
258 brxp 5071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧(𝑏 × 𝑎)𝑤 ↔ (𝑧𝑏𝑤𝑎))
259257, 258syl6ibr 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
260259ancld 574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤 → (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
261 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → 𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))
262261breqd 4594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤))
263 brin 4634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧(𝑡 ∩ (𝑏 × 𝑎))𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤))
264262, 263syl6bb 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑠𝑤 ↔ (𝑧𝑡𝑤𝑧(𝑏 × 𝑎)𝑤)))
265260, 264sylibrd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
266 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))
267266, 119syl6eqss 3618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → 𝑡𝑠)
268267ssbrd 4626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) ∧ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))) → (𝑧𝑡𝑤𝑧𝑠𝑤))
269128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → ((𝑎𝑏𝑠 = (𝑡 ∩ (𝑏 × 𝑎))) ∨ (𝑏𝑎𝑡 = (𝑠 ∩ (𝑎 × 𝑏)))))
270265, 268, 269mpjaodan 823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (𝑧𝑡𝑤𝑧𝑠𝑤))
271238, 270syl5bir 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) ∧ ((𝑤𝑠𝑦𝑤 = 𝑦) ∧ 𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
272271exp32 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑎𝑊𝑠𝑏𝑊𝑡)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
273272expr 641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑎𝑊𝑠) → (𝑏𝑊𝑡 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑦𝑎 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
274273com24 93 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑎𝑊𝑠) → (𝑦𝑎 → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))))
275274impr 647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ((𝑤𝑠𝑦𝑤 = 𝑦) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))))
276275imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
277276exlimdv 1848 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑏 𝑏𝑊𝑡 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
27871, 277syl5bi 231 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑡 ∈ ran 𝑊 → (⟨𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤)))
279278rexlimdv 3012 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (∃𝑡 ∈ ran 𝑊𝑧, 𝑤⟩ ∈ 𝑡𝑧𝑠𝑤))
280237, 279syl5bi 231 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑤𝑠𝑦𝑤 = 𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
281234, 280sylan2 490 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤 = 𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
282281ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
283282alrimiv 1842 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)))
284 vex 3176 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ V
285 breq2 4587 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧 ran 𝑊 𝑦))
286 breq2 4587 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑦 → (𝑧𝑠𝑤𝑧𝑠𝑦))
287285, 286imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → ((𝑧 ran 𝑊 𝑤𝑧𝑠𝑤) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦)))
288284, 287ceqsalv 3206 . . . . . . . . . . . . . . . . . . 19 (∀𝑤(𝑤 = 𝑦 → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤)) ↔ (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
289283, 288sylib 207 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
290198ad2antrl 760 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ∈ ran 𝑊)
291290, 201syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → 𝑠 ran 𝑊)
292291ssbrd 4626 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧𝑠𝑦𝑧 ran 𝑊 𝑦))
293289, 292impbid 201 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ran 𝑊 𝑦𝑧𝑠𝑦))
294 vex 3176 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ V
295294eliniseg 5413 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦))
296284, 295ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ran 𝑊 𝑦)
297294eliniseg 5413 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ V → (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦))
298284, 297ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑠 “ {𝑦}) ↔ 𝑧𝑠𝑦)
299293, 296, 2983bitr4g 302 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (𝑧 ∈ ( ran 𝑊 “ {𝑦}) ↔ 𝑧 ∈ (𝑠 “ {𝑦})))
300299eqrdv 2608 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 “ {𝑦}) = (𝑠 “ {𝑦}))
301233, 300sylan9eqr 2666 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → 𝑢 = (𝑠 “ {𝑦}))
302301sqxpeqd 5065 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢 × 𝑢) = ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
303302ineq2d 3776 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
304 inss2 3796 . . . . . . . . . . . . . . . . . 18 ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))
305 relxp 5150 . . . . . . . . . . . . . . . . . 18 Rel ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))
306 relss 5129 . . . . . . . . . . . . . . . . . 18 (( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → (Rel ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
307304, 305, 306mp2 9 . . . . . . . . . . . . . . . . 17 Rel ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
308 inss2 3796 . . . . . . . . . . . . . . . . . 18 (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))
309 relss 5129 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ⊆ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → (Rel ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})) → Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
310308, 305, 309mp2 9 . . . . . . . . . . . . . . . . 17 Rel (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))
311 vex 3176 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤 ∈ V
312311eliniseg 5413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ V → (𝑤 ∈ (𝑠 “ {𝑦}) ↔ 𝑤𝑠𝑦))
313297, 312anbi12d 743 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ V → ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦)))
314284, 313ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ↔ (𝑧𝑠𝑦𝑤𝑠𝑦))
315 orc 399 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑠𝑦 → (𝑤𝑠𝑦𝑤 = 𝑦))
316315, 280sylan2 490 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑤𝑠𝑦) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
317316adantrl 748 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
318291adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → 𝑠 ran 𝑊)
319318ssbrd 4626 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧𝑠𝑤𝑧 ran 𝑊 𝑤))
320317, 319impbid 201 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧𝑠𝑦𝑤𝑠𝑦)) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
321314, 320sylan2b 491 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}))) → (𝑧 ran 𝑊 𝑤𝑧𝑠𝑤))
322321pm5.32da 671 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤)))
323 brinxp2 5103 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧 ran 𝑊 𝑤))
324 df-br 4584 . . . . . . . . . . . . . . . . . . 19 (𝑧( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
325 df-3an 1033 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧 ran 𝑊 𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
326323, 324, 3253bitr3i 289 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧 ran 𝑊 𝑤))
327 brinxp2 5103 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ (𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧𝑠𝑤))
328 df-br 4584 . . . . . . . . . . . . . . . . . . 19 (𝑧(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))𝑤 ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
329 df-3an 1033 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦}) ∧ 𝑧𝑠𝑤) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
330327, 328, 3293bitr3i 289 . . . . . . . . . . . . . . . . . 18 (⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ((𝑧 ∈ (𝑠 “ {𝑦}) ∧ 𝑤 ∈ (𝑠 “ {𝑦})) ∧ 𝑧𝑠𝑤))
331322, 326, 3303bitr4g 302 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → (⟨𝑧, 𝑤⟩ ∈ ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
332307, 310, 331eqrelrdv 5139 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
333332adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
334303, 333eqtrd 2644 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ( ran 𝑊 ∩ (𝑢 × 𝑢)) = (𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦}))))
335301, 334oveq12d 6567 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → (𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))))
336335eqeq1d 2612 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) ∧ 𝑢 = ( ran 𝑊 “ {𝑦})) → ((𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
337232, 336sbcied 3439 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → ([( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ((𝑠 “ {𝑦})𝐹(𝑠 ∩ ((𝑠 “ {𝑦}) × (𝑠 “ {𝑦})))) = 𝑦))
338222, 337mpbird 246 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑊𝑠𝑦𝑎)) → [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
339338exp32 629 . . . . . . . . 9 (𝜑 → (𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
340339exlimdv 1848 . . . . . . . 8 (𝜑 → (∃𝑠 𝑎𝑊𝑠 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
3413, 340syl5bi 231 . . . . . . 7 (𝜑 → (𝑎 ∈ dom 𝑊 → (𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)))
342341rexlimdv 3012 . . . . . 6 (𝜑 → (∃𝑎 ∈ dom 𝑊 𝑦𝑎[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
34344, 342syl5bi 231 . . . . 5 (𝜑 → (𝑦𝑋[( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
344343ralrimiv 2948 . . . 4 (𝜑 → ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦)
345217, 344jca 553 . . 3 (𝜑 → ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))
3464, 5fpwwe2lem2 9333 . . 3 (𝜑 → (𝑋𝑊 ran 𝑊 ↔ ((𝑋𝐴 ran 𝑊 ⊆ (𝑋 × 𝑋)) ∧ ( ran 𝑊 We 𝑋 ∧ ∀𝑦𝑋 [( ran 𝑊 “ {𝑦}) / 𝑢](𝑢𝐹( ran 𝑊 ∩ (𝑢 × 𝑢))) = 𝑦))))
34738, 345, 346mpbir2and 959 . 2 (𝜑𝑋𝑊 ran 𝑊)
34821releldmi 5283 . 2 (𝑋𝑊 ran 𝑊𝑋 ∈ dom 𝑊)
349347, 348syl 17 1 (𝜑𝑋 ∈ dom 𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  w3o 1030  w3a 1031  wal 1473   = wceq 1475  wex 1695  wcel 1977  wne 2780  wral 2896  wrex 2897  Vcvv 3173  [wsbc 3402  cin 3539  wss 3540  c0 3874  𝒫 cpw 4108  {csn 4125  cop 4131   cuni 4372   class class class wbr 4583  {copab 4642   Or wor 4958   Fr wfr 4994   We wwe 4996   × cxp 5036  ccnv 5037  dom cdm 5038  ran crn 5039  cima 5041  Rel wrel 5043  (class class class)co 6549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-wrecs 7294  df-recs 7355  df-oi 8298
This theorem is referenced by:  fpwwe2lem13  9343  fpwwe2  9344
  Copyright terms: Public domain W3C validator