Metamath Proof Explorer


Theorem fpwwe2lem11

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
fpwwe2.2 ( 𝜑𝐴𝑉 )
fpwwe2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
fpwwe2.4 𝑋 = dom 𝑊
Assertion fpwwe2lem11 ( 𝜑𝑋 ∈ dom 𝑊 )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ( 𝜑𝐴𝑉 )
3 fpwwe2.3 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2.4 𝑋 = dom 𝑊
5 vex 𝑎 ∈ V
6 5 eldm ( 𝑎 ∈ dom 𝑊 ↔ ∃ 𝑠 𝑎 𝑊 𝑠 )
7 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑎 𝑊 𝑠 ↔ ( ( 𝑎𝐴𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑦𝑎 [ ( 𝑠 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑠 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
8 7 simprbda ( ( 𝜑𝑎 𝑊 𝑠 ) → ( 𝑎𝐴𝑠 ⊆ ( 𝑎 × 𝑎 ) ) )
9 8 simpld ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑎𝐴 )
10 velpw ( 𝑎 ∈ 𝒫 𝐴𝑎𝐴 )
11 9 10 sylibr ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑎 ∈ 𝒫 𝐴 )
12 11 ex ( 𝜑 → ( 𝑎 𝑊 𝑠𝑎 ∈ 𝒫 𝐴 ) )
13 12 exlimdv ( 𝜑 → ( ∃ 𝑠 𝑎 𝑊 𝑠𝑎 ∈ 𝒫 𝐴 ) )
14 6 13 syl5bi ( 𝜑 → ( 𝑎 ∈ dom 𝑊𝑎 ∈ 𝒫 𝐴 ) )
15 14 ssrdv ( 𝜑 → dom 𝑊 ⊆ 𝒫 𝐴 )
16 sspwuni ( dom 𝑊 ⊆ 𝒫 𝐴 dom 𝑊𝐴 )
17 15 16 sylib ( 𝜑 dom 𝑊𝐴 )
18 4 17 eqsstrid ( 𝜑𝑋𝐴 )
19 vex 𝑠 ∈ V
20 19 elrn ( 𝑠 ∈ ran 𝑊 ↔ ∃ 𝑎 𝑎 𝑊 𝑠 )
21 8 simprd ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑠 ⊆ ( 𝑎 × 𝑎 ) )
22 1 relopabiv Rel 𝑊
23 22 releldmi ( 𝑎 𝑊 𝑠𝑎 ∈ dom 𝑊 )
24 23 adantl ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑎 ∈ dom 𝑊 )
25 elssuni ( 𝑎 ∈ dom 𝑊𝑎 dom 𝑊 )
26 24 25 syl ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑎 dom 𝑊 )
27 26 4 sseqtrrdi ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑎𝑋 )
28 xpss12 ( ( 𝑎𝑋𝑎𝑋 ) → ( 𝑎 × 𝑎 ) ⊆ ( 𝑋 × 𝑋 ) )
29 27 27 28 syl2anc ( ( 𝜑𝑎 𝑊 𝑠 ) → ( 𝑎 × 𝑎 ) ⊆ ( 𝑋 × 𝑋 ) )
30 21 29 sstrd ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑠 ⊆ ( 𝑋 × 𝑋 ) )
31 velpw ( 𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ↔ 𝑠 ⊆ ( 𝑋 × 𝑋 ) )
32 30 31 sylibr ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) )
33 32 ex ( 𝜑 → ( 𝑎 𝑊 𝑠𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) )
34 33 exlimdv ( 𝜑 → ( ∃ 𝑎 𝑎 𝑊 𝑠𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) )
35 20 34 syl5bi ( 𝜑 → ( 𝑠 ∈ ran 𝑊𝑠 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) )
36 35 ssrdv ( 𝜑 → ran 𝑊 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
37 sspwuni ( ran 𝑊 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ↔ ran 𝑊 ⊆ ( 𝑋 × 𝑋 ) )
38 36 37 sylib ( 𝜑 ran 𝑊 ⊆ ( 𝑋 × 𝑋 ) )
39 18 38 jca ( 𝜑 → ( 𝑋𝐴 ran 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) )
40 n0 ( 𝑛 ≠ ∅ ↔ ∃ 𝑦 𝑦𝑛 )
41 ssel2 ( ( 𝑛𝑋𝑦𝑛 ) → 𝑦𝑋 )
42 41 adantl ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → 𝑦𝑋 )
43 4 eleq2i ( 𝑦𝑋𝑦 dom 𝑊 )
44 eluni2 ( 𝑦 dom 𝑊 ↔ ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎 )
45 43 44 bitri ( 𝑦𝑋 ↔ ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎 )
46 42 45 sylib ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎 )
47 5 inex2 ( 𝑛𝑎 ) ∈ V
48 47 a1i ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑛𝑎 ) ∈ V )
49 7 simplbda ( ( 𝜑𝑎 𝑊 𝑠 ) → ( 𝑠 We 𝑎 ∧ ∀ 𝑦𝑎 [ ( 𝑠 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑠 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
50 49 simpld ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑠 We 𝑎 )
51 50 ad2ant2r ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑠 We 𝑎 )
52 wefr ( 𝑠 We 𝑎𝑠 Fr 𝑎 )
53 51 52 syl ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑠 Fr 𝑎 )
54 inss2 ( 𝑛𝑎 ) ⊆ 𝑎
55 54 a1i ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑛𝑎 ) ⊆ 𝑎 )
56 simplrr ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑦𝑛 )
57 simprr ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑦𝑎 )
58 inelcm ( ( 𝑦𝑛𝑦𝑎 ) → ( 𝑛𝑎 ) ≠ ∅ )
59 56 57 58 syl2anc ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑛𝑎 ) ≠ ∅ )
60 fri ( ( ( ( 𝑛𝑎 ) ∈ V ∧ 𝑠 Fr 𝑎 ) ∧ ( ( 𝑛𝑎 ) ⊆ 𝑎 ∧ ( 𝑛𝑎 ) ≠ ∅ ) ) → ∃ 𝑣 ∈ ( 𝑛𝑎 ) ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 )
61 48 53 55 59 60 syl22anc ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ∃ 𝑣 ∈ ( 𝑛𝑎 ) ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 )
62 simprl ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) → 𝑣 ∈ ( 𝑛𝑎 ) )
63 62 elin1d ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) → 𝑣𝑛 )
64 simplrr ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 )
65 ralnex ( ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ↔ ¬ ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 )
66 64 65 sylib ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ¬ ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 )
67 df-br ( 𝑤 ran 𝑊 𝑣 ↔ ⟨ 𝑤 , 𝑣 ⟩ ∈ ran 𝑊 )
68 eluni2 ( ⟨ 𝑤 , 𝑣 ⟩ ∈ ran 𝑊 ↔ ∃ 𝑡 ∈ ran 𝑊𝑤 , 𝑣 ⟩ ∈ 𝑡 )
69 67 68 bitri ( 𝑤 ran 𝑊 𝑣 ↔ ∃ 𝑡 ∈ ran 𝑊𝑤 , 𝑣 ⟩ ∈ 𝑡 )
70 vex 𝑡 ∈ V
71 70 elrn ( 𝑡 ∈ ran 𝑊 ↔ ∃ 𝑏 𝑏 𝑊 𝑡 )
72 df-br ( 𝑤 𝑡 𝑣 ↔ ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 )
73 simprll ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑤𝑛 )
74 73 adantr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤𝑛 )
75 simprr ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑤 𝑡 𝑣 )
76 simp-4l ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝜑 )
77 simprl ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑎 𝑊 𝑠 )
78 77 ad2antrr ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑎 𝑊 𝑠 )
79 simprlr ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑏 𝑊 𝑡 )
80 simprr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑏 𝑊 𝑡 )
81 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑏 𝑊 𝑡 ↔ ( ( 𝑏𝐴𝑡 ⊆ ( 𝑏 × 𝑏 ) ) ∧ ( 𝑡 We 𝑏 ∧ ∀ 𝑦𝑏 [ ( 𝑡 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑡 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
82 81 adantr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( 𝑏 𝑊 𝑡 ↔ ( ( 𝑏𝐴𝑡 ⊆ ( 𝑏 × 𝑏 ) ) ∧ ( 𝑡 We 𝑏 ∧ ∀ 𝑦𝑏 [ ( 𝑡 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑡 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
83 80 82 mpbid ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( ( 𝑏𝐴𝑡 ⊆ ( 𝑏 × 𝑏 ) ) ∧ ( 𝑡 We 𝑏 ∧ ∀ 𝑦𝑏 [ ( 𝑡 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑡 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
84 83 simpld ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( 𝑏𝐴𝑡 ⊆ ( 𝑏 × 𝑏 ) ) )
85 84 simprd ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑡 ⊆ ( 𝑏 × 𝑏 ) )
86 76 78 79 85 syl12anc ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑡 ⊆ ( 𝑏 × 𝑏 ) )
87 86 ssbrd ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → ( 𝑤 𝑡 𝑣𝑤 ( 𝑏 × 𝑏 ) 𝑣 ) )
88 75 87 mpd ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑤 ( 𝑏 × 𝑏 ) 𝑣 )
89 brxp ( 𝑤 ( 𝑏 × 𝑏 ) 𝑣 ↔ ( 𝑤𝑏𝑣𝑏 ) )
90 89 simplbi ( 𝑤 ( 𝑏 × 𝑏 ) 𝑣𝑤𝑏 )
91 88 90 syl ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑤𝑏 )
92 91 adantr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤𝑏 )
93 62 elin2d ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) → 𝑣𝑎 )
94 93 ad2antrr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑣𝑎 )
95 simplrr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤 𝑡 𝑣 )
96 brinxp2 ( 𝑤 ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) 𝑣 ↔ ( ( 𝑤𝑏𝑣𝑎 ) ∧ 𝑤 𝑡 𝑣 ) )
97 92 94 95 96 syl21anbrc ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤 ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) 𝑣 )
98 simprr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) )
99 98 breqd ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑤 𝑠 𝑣𝑤 ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) 𝑣 ) )
100 97 99 mpbird ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤 𝑠 𝑣 )
101 76 78 21 syl2anc ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → 𝑠 ⊆ ( 𝑎 × 𝑎 ) )
102 101 adantr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑠 ⊆ ( 𝑎 × 𝑎 ) )
103 102 ssbrd ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑤 𝑠 𝑣𝑤 ( 𝑎 × 𝑎 ) 𝑣 ) )
104 100 103 mpd ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤 ( 𝑎 × 𝑎 ) 𝑣 )
105 brxp ( 𝑤 ( 𝑎 × 𝑎 ) 𝑣 ↔ ( 𝑤𝑎𝑣𝑎 ) )
106 105 simplbi ( 𝑤 ( 𝑎 × 𝑎 ) 𝑣𝑤𝑎 )
107 104 106 syl ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤𝑎 )
108 74 107 elind ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤 ∈ ( 𝑛𝑎 ) )
109 breq1 ( 𝑧 = 𝑤 → ( 𝑧 𝑠 𝑣𝑤 𝑠 𝑣 ) )
110 109 rspcev ( ( 𝑤 ∈ ( 𝑛𝑎 ) ∧ 𝑤 𝑠 𝑣 ) → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 )
111 108 100 110 syl2anc ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 )
112 73 adantr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤𝑛 )
113 simprl ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑏𝑎 )
114 91 adantr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤𝑏 )
115 113 114 sseldd ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤𝑎 )
116 112 115 elind ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤 ∈ ( 𝑛𝑎 ) )
117 simplrr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤 𝑡 𝑣 )
118 simprr ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) )
119 inss1 ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ⊆ 𝑠
120 118 119 eqsstrdi ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑡𝑠 )
121 120 ssbrd ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑤 𝑡 𝑣𝑤 𝑠 𝑣 ) )
122 117 121 mpd ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤 𝑠 𝑣 )
123 116 122 110 syl2anc ( ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 )
124 2 adantr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝐴𝑉 )
125 3 adantlr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
126 simprl ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑎 𝑊 𝑠 )
127 1 124 125 126 80 fpwwe2lem9 ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ∨ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) )
128 76 78 79 127 syl12anc ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → ( ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ∨ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) )
129 111 123 128 mpjaodan ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( ( 𝑤𝑛𝑏 𝑊 𝑡 ) ∧ 𝑤 𝑡 𝑣 ) ) → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 )
130 129 expr ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( 𝑤𝑛𝑏 𝑊 𝑡 ) ) → ( 𝑤 𝑡 𝑣 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) )
131 72 130 syl5bir ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( 𝑤𝑛𝑏 𝑊 𝑡 ) ) → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) )
132 131 expr ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) ) )
133 132 exlimdv ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ( ∃ 𝑏 𝑏 𝑊 𝑡 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) ) )
134 71 133 syl5bi ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ( 𝑡 ∈ ran 𝑊 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) ) )
135 134 rexlimdv ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ( ∃ 𝑡 ∈ ran 𝑊𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) )
136 69 135 syl5bi ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ( 𝑤 ran 𝑊 𝑣 → ∃ 𝑧 ∈ ( 𝑛𝑎 ) 𝑧 𝑠 𝑣 ) )
137 66 136 mtod ( ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤𝑛 ) → ¬ 𝑤 ran 𝑊 𝑣 )
138 137 ralrimiva ( ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) → ∀ 𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 )
139 61 63 138 reximssdv ( ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 )
140 139 exp32 ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → ( 𝑎 𝑊 𝑠 → ( 𝑦𝑎 → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) ) )
141 140 exlimdv ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → ( ∃ 𝑠 𝑎 𝑊 𝑠 → ( 𝑦𝑎 → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) ) )
142 6 141 syl5bi ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → ( 𝑎 ∈ dom 𝑊 → ( 𝑦𝑎 → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) ) )
143 142 rexlimdv ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → ( ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎 → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
144 46 143 mpd ( ( 𝜑 ∧ ( 𝑛𝑋𝑦𝑛 ) ) → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 )
145 144 expr ( ( 𝜑𝑛𝑋 ) → ( 𝑦𝑛 → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
146 145 exlimdv ( ( 𝜑𝑛𝑋 ) → ( ∃ 𝑦 𝑦𝑛 → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
147 40 146 syl5bi ( ( 𝜑𝑛𝑋 ) → ( 𝑛 ≠ ∅ → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
148 147 expimpd ( 𝜑 → ( ( 𝑛𝑋𝑛 ≠ ∅ ) → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
149 148 alrimiv ( 𝜑 → ∀ 𝑛 ( ( 𝑛𝑋𝑛 ≠ ∅ ) → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
150 df-fr ( ran 𝑊 Fr 𝑋 ↔ ∀ 𝑛 ( ( 𝑛𝑋𝑛 ≠ ∅ ) → ∃ 𝑣𝑛𝑤𝑛 ¬ 𝑤 ran 𝑊 𝑣 ) )
151 149 150 sylibr ( 𝜑 ran 𝑊 Fr 𝑋 )
152 4 eleq2i ( 𝑤𝑋𝑤 dom 𝑊 )
153 eluni2 ( 𝑤 dom 𝑊 ↔ ∃ 𝑏 ∈ dom 𝑊 𝑤𝑏 )
154 152 153 bitri ( 𝑤𝑋 ↔ ∃ 𝑏 ∈ dom 𝑊 𝑤𝑏 )
155 45 154 anbi12i ( ( 𝑦𝑋𝑤𝑋 ) ↔ ( ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃ 𝑏 ∈ dom 𝑊 𝑤𝑏 ) )
156 reeanv ( ∃ 𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊 ( 𝑦𝑎𝑤𝑏 ) ↔ ( ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎 ∧ ∃ 𝑏 ∈ dom 𝑊 𝑤𝑏 ) )
157 155 156 bitr4i ( ( 𝑦𝑋𝑤𝑋 ) ↔ ∃ 𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊 ( 𝑦𝑎𝑤𝑏 ) )
158 vex 𝑏 ∈ V
159 158 eldm ( 𝑏 ∈ dom 𝑊 ↔ ∃ 𝑡 𝑏 𝑊 𝑡 )
160 6 159 anbi12i ( ( 𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊 ) ↔ ( ∃ 𝑠 𝑎 𝑊 𝑠 ∧ ∃ 𝑡 𝑏 𝑊 𝑡 ) )
161 exdistrv ( ∃ 𝑠𝑡 ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ↔ ( ∃ 𝑠 𝑎 𝑊 𝑠 ∧ ∃ 𝑡 𝑏 𝑊 𝑡 ) )
162 160 161 bitr4i ( ( 𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊 ) ↔ ∃ 𝑠𝑡 ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) )
163 83 simprd ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( 𝑡 We 𝑏 ∧ ∀ 𝑦𝑏 [ ( 𝑡 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑡 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
164 163 simpld ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑡 We 𝑏 )
165 164 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑡 We 𝑏 )
166 weso ( 𝑡 We 𝑏𝑡 Or 𝑏 )
167 165 166 syl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑡 Or 𝑏 )
168 simprl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑎𝑏 )
169 simplrl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑦𝑎 )
170 168 169 sseldd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑦𝑏 )
171 simplrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤𝑏 )
172 solin ( ( 𝑡 Or 𝑏 ∧ ( 𝑦𝑏𝑤𝑏 ) ) → ( 𝑦 𝑡 𝑤𝑦 = 𝑤𝑤 𝑡 𝑦 ) )
173 167 170 171 172 syl12anc ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑦 𝑡 𝑤𝑦 = 𝑤𝑤 𝑡 𝑦 ) )
174 22 relelrni ( 𝑏 𝑊 𝑡𝑡 ∈ ran 𝑊 )
175 174 ad2antll ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑡 ∈ ran 𝑊 )
176 175 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑡 ∈ ran 𝑊 )
177 elssuni ( 𝑡 ∈ ran 𝑊𝑡 ran 𝑊 )
178 176 177 syl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑡 ran 𝑊 )
179 178 ssbrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑦 𝑡 𝑤𝑦 ran 𝑊 𝑤 ) )
180 idd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑦 = 𝑤𝑦 = 𝑤 ) )
181 178 ssbrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑤 𝑡 𝑦𝑤 ran 𝑊 𝑦 ) )
182 179 180 181 3orim123d ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( ( 𝑦 𝑡 𝑤𝑦 = 𝑤𝑤 𝑡 𝑦 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) )
183 173 182 mpd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) )
184 50 adantrr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑠 We 𝑎 )
185 184 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑠 We 𝑎 )
186 weso ( 𝑠 We 𝑎𝑠 Or 𝑎 )
187 185 186 syl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑠 Or 𝑎 )
188 simplrl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑦𝑎 )
189 simprl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑏𝑎 )
190 simplrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤𝑏 )
191 189 190 sseldd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑤𝑎 )
192 solin ( ( 𝑠 Or 𝑎 ∧ ( 𝑦𝑎𝑤𝑎 ) ) → ( 𝑦 𝑠 𝑤𝑦 = 𝑤𝑤 𝑠 𝑦 ) )
193 187 188 191 192 syl12anc ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑦 𝑠 𝑤𝑦 = 𝑤𝑤 𝑠 𝑦 ) )
194 22 relelrni ( 𝑎 𝑊 𝑠𝑠 ∈ ran 𝑊 )
195 194 ad2antrl ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑠 ∈ ran 𝑊 )
196 195 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑠 ∈ ran 𝑊 )
197 elssuni ( 𝑠 ∈ ran 𝑊𝑠 ran 𝑊 )
198 196 197 syl ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑠 ran 𝑊 )
199 198 ssbrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑦 𝑠 𝑤𝑦 ran 𝑊 𝑤 ) )
200 idd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑦 = 𝑤𝑦 = 𝑤 ) )
201 198 ssbrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑤 𝑠 𝑦𝑤 ran 𝑊 𝑦 ) )
202 199 200 201 3orim123d ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( ( 𝑦 𝑠 𝑤𝑦 = 𝑤𝑤 𝑠 𝑦 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) )
203 193 202 mpd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) )
204 127 adantr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) → ( ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ∨ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) )
205 183 203 204 mpjaodan ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑦𝑎𝑤𝑏 ) ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) )
206 205 exp31 ( 𝜑 → ( ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) → ( ( 𝑦𝑎𝑤𝑏 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) ) )
207 206 exlimdvv ( 𝜑 → ( ∃ 𝑠𝑡 ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) → ( ( 𝑦𝑎𝑤𝑏 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) ) )
208 162 207 syl5bi ( 𝜑 → ( ( 𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊 ) → ( ( 𝑦𝑎𝑤𝑏 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) ) )
209 208 rexlimdvv ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊𝑏 ∈ dom 𝑊 ( 𝑦𝑎𝑤𝑏 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) )
210 157 209 syl5bi ( 𝜑 → ( ( 𝑦𝑋𝑤𝑋 ) → ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) )
211 210 ralrimivv ( 𝜑 → ∀ 𝑦𝑋𝑤𝑋 ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) )
212 dfwe2 ( ran 𝑊 We 𝑋 ↔ ( ran 𝑊 Fr 𝑋 ∧ ∀ 𝑦𝑋𝑤𝑋 ( 𝑦 ran 𝑊 𝑤𝑦 = 𝑤𝑤 ran 𝑊 𝑦 ) ) )
213 151 211 212 sylanbrc ( 𝜑 ran 𝑊 We 𝑋 )
214 1 fpwwe2cbv 𝑊 = { ⟨ 𝑧 , 𝑡 ⟩ ∣ ( ( 𝑧𝐴𝑡 ⊆ ( 𝑧 × 𝑧 ) ) ∧ ( 𝑡 We 𝑧 ∧ ∀ 𝑤𝑧 [ ( 𝑡 “ { 𝑤 } ) / 𝑏 ] ( 𝑏 𝐹 ( 𝑡 ∩ ( 𝑏 × 𝑏 ) ) ) = 𝑤 ) ) }
215 2 adantr ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝐴𝑉 )
216 simpr ( ( 𝜑𝑎 𝑊 𝑠 ) → 𝑎 𝑊 𝑠 )
217 214 215 216 fpwwe2lem3 ( ( ( 𝜑𝑎 𝑊 𝑠 ) ∧ 𝑦𝑎 ) → ( ( 𝑠 “ { 𝑦 } ) 𝐹 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ) = 𝑦 )
218 217 anasss ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ( 𝑠 “ { 𝑦 } ) 𝐹 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ) = 𝑦 )
219 cnvimass ( ran 𝑊 “ { 𝑦 } ) ⊆ dom ran 𝑊
220 2 18 ssexd ( 𝜑𝑋 ∈ V )
221 220 220 xpexd ( 𝜑 → ( 𝑋 × 𝑋 ) ∈ V )
222 221 38 ssexd ( 𝜑 ran 𝑊 ∈ V )
223 222 adantr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ran 𝑊 ∈ V )
224 223 dmexd ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → dom ran 𝑊 ∈ V )
225 ssexg ( ( ( ran 𝑊 “ { 𝑦 } ) ⊆ dom ran 𝑊 ∧ dom ran 𝑊 ∈ V ) → ( ran 𝑊 “ { 𝑦 } ) ∈ V )
226 219 224 225 sylancr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ran 𝑊 “ { 𝑦 } ) ∈ V )
227 id ( 𝑢 = ( ran 𝑊 “ { 𝑦 } ) → 𝑢 = ( ran 𝑊 “ { 𝑦 } ) )
228 olc ( 𝑤 = 𝑦 → ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) )
229 df-br ( 𝑧 ran 𝑊 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ran 𝑊 )
230 eluni2 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ran 𝑊 ↔ ∃ 𝑡 ∈ ran 𝑊𝑧 , 𝑤 ⟩ ∈ 𝑡 )
231 229 230 bitri ( 𝑧 ran 𝑊 𝑤 ↔ ∃ 𝑡 ∈ ran 𝑊𝑧 , 𝑤 ⟩ ∈ 𝑡 )
232 df-br ( 𝑧 𝑡 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 )
233 85 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑡 ⊆ ( 𝑏 × 𝑏 ) )
234 233 ssbrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤𝑧 ( 𝑏 × 𝑏 ) 𝑤 ) )
235 brxp ( 𝑧 ( 𝑏 × 𝑏 ) 𝑤 ↔ ( 𝑧𝑏𝑤𝑏 ) )
236 235 simplbi ( 𝑧 ( 𝑏 × 𝑏 ) 𝑤𝑧𝑏 )
237 234 236 syl6 ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤𝑧𝑏 ) )
238 21 adantrr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → 𝑠 ⊆ ( 𝑎 × 𝑎 ) )
239 238 ssbrd ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( 𝑤 𝑠 𝑦𝑤 ( 𝑎 × 𝑎 ) 𝑦 ) )
240 239 imp ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ 𝑤 𝑠 𝑦 ) → 𝑤 ( 𝑎 × 𝑎 ) 𝑦 )
241 brxp ( 𝑤 ( 𝑎 × 𝑎 ) 𝑦 ↔ ( 𝑤𝑎𝑦𝑎 ) )
242 241 simplbi ( 𝑤 ( 𝑎 × 𝑎 ) 𝑦𝑤𝑎 )
243 240 242 syl ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ 𝑤 𝑠 𝑦 ) → 𝑤𝑎 )
244 243 a1d ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ 𝑤 𝑠 𝑦 ) → ( 𝑦𝑎𝑤𝑎 ) )
245 elequ1 ( 𝑤 = 𝑦 → ( 𝑤𝑎𝑦𝑎 ) )
246 245 biimprd ( 𝑤 = 𝑦 → ( 𝑦𝑎𝑤𝑎 ) )
247 246 adantl ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ 𝑤 = 𝑦 ) → ( 𝑦𝑎𝑤𝑎 ) )
248 244 247 jaodan ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ) → ( 𝑦𝑎𝑤𝑎 ) )
249 248 impr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) → 𝑤𝑎 )
250 249 adantr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑤𝑎 )
251 237 250 jctird ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤 → ( 𝑧𝑏𝑤𝑎 ) ) )
252 brxp ( 𝑧 ( 𝑏 × 𝑎 ) 𝑤 ↔ ( 𝑧𝑏𝑤𝑎 ) )
253 251 252 syl6ibr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤𝑧 ( 𝑏 × 𝑎 ) 𝑤 ) )
254 253 ancld ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤 → ( 𝑧 𝑡 𝑤𝑧 ( 𝑏 × 𝑎 ) 𝑤 ) ) )
255 simprr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → 𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) )
256 255 breqd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑠 𝑤𝑧 ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) 𝑤 ) )
257 brin ( 𝑧 ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) 𝑤 ↔ ( 𝑧 𝑡 𝑤𝑧 ( 𝑏 × 𝑎 ) 𝑤 ) )
258 256 257 bitrdi ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑠 𝑤 ↔ ( 𝑧 𝑡 𝑤𝑧 ( 𝑏 × 𝑎 ) 𝑤 ) ) )
259 254 258 sylibrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤𝑧 𝑠 𝑤 ) )
260 simprr ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) )
261 260 119 eqsstrdi ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → 𝑡𝑠 )
262 261 ssbrd ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) ∧ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) → ( 𝑧 𝑡 𝑤𝑧 𝑠 𝑤 ) )
263 127 adantr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) → ( ( 𝑎𝑏𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ∨ ( 𝑏𝑎𝑡 = ( 𝑠 ∩ ( 𝑎 × 𝑏 ) ) ) ) )
264 259 262 263 mpjaodan ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) → ( 𝑧 𝑡 𝑤𝑧 𝑠 𝑤 ) )
265 232 264 syl5bir ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ∧ 𝑦𝑎 ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) )
266 265 exp32 ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑏 𝑊 𝑡 ) ) → ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) → ( 𝑦𝑎 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) ) )
267 266 expr ( ( 𝜑𝑎 𝑊 𝑠 ) → ( 𝑏 𝑊 𝑡 → ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) → ( 𝑦𝑎 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) ) ) )
268 267 com24 ( ( 𝜑𝑎 𝑊 𝑠 ) → ( 𝑦𝑎 → ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) ) ) )
269 268 impr ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) ) )
270 269 imp ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) )
271 270 exlimdv ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ) → ( ∃ 𝑏 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) )
272 71 271 syl5bi ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ) → ( 𝑡 ∈ ran 𝑊 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) ) )
273 272 rexlimdv ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ) → ( ∃ 𝑡 ∈ ran 𝑊𝑧 , 𝑤 ⟩ ∈ 𝑡𝑧 𝑠 𝑤 ) )
274 231 273 syl5bi ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) ) → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) )
275 228 274 sylan2 ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑤 = 𝑦 ) → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) )
276 275 ex ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑤 = 𝑦 → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) ) )
277 276 alrimiv ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ∀ 𝑤 ( 𝑤 = 𝑦 → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) ) )
278 breq2 ( 𝑤 = 𝑦 → ( 𝑧 ran 𝑊 𝑤𝑧 ran 𝑊 𝑦 ) )
279 breq2 ( 𝑤 = 𝑦 → ( 𝑧 𝑠 𝑤𝑧 𝑠 𝑦 ) )
280 278 279 imbi12d ( 𝑤 = 𝑦 → ( ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) ↔ ( 𝑧 ran 𝑊 𝑦𝑧 𝑠 𝑦 ) ) )
281 280 equsalvw ( ∀ 𝑤 ( 𝑤 = 𝑦 → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) ) ↔ ( 𝑧 ran 𝑊 𝑦𝑧 𝑠 𝑦 ) )
282 277 281 sylib ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑧 ran 𝑊 𝑦𝑧 𝑠 𝑦 ) )
283 194 ad2antrl ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑠 ∈ ran 𝑊 )
284 283 197 syl ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → 𝑠 ran 𝑊 )
285 284 ssbrd ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑧 𝑠 𝑦𝑧 ran 𝑊 𝑦 ) )
286 282 285 impbid ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑧 ran 𝑊 𝑦𝑧 𝑠 𝑦 ) )
287 vex 𝑧 ∈ V
288 287 eliniseg ( 𝑦 ∈ V → ( 𝑧 ∈ ( ran 𝑊 “ { 𝑦 } ) ↔ 𝑧 ran 𝑊 𝑦 ) )
289 288 elv ( 𝑧 ∈ ( ran 𝑊 “ { 𝑦 } ) ↔ 𝑧 ran 𝑊 𝑦 )
290 287 eliniseg ( 𝑦 ∈ V → ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ↔ 𝑧 𝑠 𝑦 ) )
291 290 elv ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ↔ 𝑧 𝑠 𝑦 )
292 286 289 291 3bitr4g ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( 𝑧 ∈ ( ran 𝑊 “ { 𝑦 } ) ↔ 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ) )
293 292 eqrdv ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ran 𝑊 “ { 𝑦 } ) = ( 𝑠 “ { 𝑦 } ) )
294 227 293 sylan9eqr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → 𝑢 = ( 𝑠 “ { 𝑦 } ) )
295 294 sqxpeqd ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → ( 𝑢 × 𝑢 ) = ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) )
296 295 ineq2d ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) = ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) )
297 relinxp Rel ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) )
298 relinxp Rel ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) )
299 vex 𝑤 ∈ V
300 299 eliniseg ( 𝑦 ∈ V → ( 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ↔ 𝑤 𝑠 𝑦 ) )
301 290 300 anbi12d ( 𝑦 ∈ V → ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ↔ ( 𝑧 𝑠 𝑦𝑤 𝑠 𝑦 ) ) )
302 301 elv ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ↔ ( 𝑧 𝑠 𝑦𝑤 𝑠 𝑦 ) )
303 orc ( 𝑤 𝑠 𝑦 → ( 𝑤 𝑠 𝑦𝑤 = 𝑦 ) )
304 303 274 sylan2 ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑤 𝑠 𝑦 ) → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) )
305 304 adantrl ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑧 𝑠 𝑦𝑤 𝑠 𝑦 ) ) → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) )
306 284 adantr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑧 𝑠 𝑦𝑤 𝑠 𝑦 ) ) → 𝑠 ran 𝑊 )
307 306 ssbrd ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑧 𝑠 𝑦𝑤 𝑠 𝑦 ) ) → ( 𝑧 𝑠 𝑤𝑧 ran 𝑊 𝑤 ) )
308 305 307 impbid ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑧 𝑠 𝑦𝑤 𝑠 𝑦 ) ) → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) )
309 302 308 sylan2b ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ) → ( 𝑧 ran 𝑊 𝑤𝑧 𝑠 𝑤 ) )
310 309 pm5.32da ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ∧ 𝑧 ran 𝑊 𝑤 ) ↔ ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ∧ 𝑧 𝑠 𝑤 ) ) )
311 df-br ( 𝑧 ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) )
312 brinxp2 ( 𝑧 ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) 𝑤 ↔ ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ∧ 𝑧 ran 𝑊 𝑤 ) )
313 311 312 bitr3i ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ↔ ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ∧ 𝑧 ran 𝑊 𝑤 ) )
314 df-br ( 𝑧 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) 𝑤 ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) )
315 brinxp2 ( 𝑧 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) 𝑤 ↔ ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ∧ 𝑧 𝑠 𝑤 ) )
316 314 315 bitr3i ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ↔ ( ( 𝑧 ∈ ( 𝑠 “ { 𝑦 } ) ∧ 𝑤 ∈ ( 𝑠 “ { 𝑦 } ) ) ∧ 𝑧 𝑠 𝑤 ) )
317 310 313 316 3bitr4g ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ) )
318 297 298 317 eqrelrdv ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) = ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) )
319 318 adantr ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → ( ran 𝑊 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) = ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) )
320 296 319 eqtrd ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) = ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) )
321 294 320 oveq12d ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = ( ( 𝑠 “ { 𝑦 } ) 𝐹 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ) )
322 321 eqeq1d ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) ∧ 𝑢 = ( ran 𝑊 “ { 𝑦 } ) ) → ( ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( ( 𝑠 “ { 𝑦 } ) 𝐹 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ) = 𝑦 ) )
323 226 322 sbcied ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → ( [ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( ( 𝑠 “ { 𝑦 } ) 𝐹 ( 𝑠 ∩ ( ( 𝑠 “ { 𝑦 } ) × ( 𝑠 “ { 𝑦 } ) ) ) ) = 𝑦 ) )
324 218 323 mpbird ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠𝑦𝑎 ) ) → [ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
325 324 exp32 ( 𝜑 → ( 𝑎 𝑊 𝑠 → ( 𝑦𝑎[ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
326 325 exlimdv ( 𝜑 → ( ∃ 𝑠 𝑎 𝑊 𝑠 → ( 𝑦𝑎[ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
327 6 326 syl5bi ( 𝜑 → ( 𝑎 ∈ dom 𝑊 → ( 𝑦𝑎[ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
328 327 rexlimdv ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊 𝑦𝑎[ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
329 45 328 syl5bi ( 𝜑 → ( 𝑦𝑋[ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
330 329 ralrimiv ( 𝜑 → ∀ 𝑦𝑋 [ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
331 213 330 jca ( 𝜑 → ( ran 𝑊 We 𝑋 ∧ ∀ 𝑦𝑋 [ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
332 1 2 fpwwe2lem2 ( 𝜑 → ( 𝑋 𝑊 ran 𝑊 ↔ ( ( 𝑋𝐴 ran 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( ran 𝑊 We 𝑋 ∧ ∀ 𝑦𝑋 [ ( ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
333 39 331 332 mpbir2and ( 𝜑𝑋 𝑊 ran 𝑊 )
334 22 releldmi ( 𝑋 𝑊 ran 𝑊𝑋 ∈ dom 𝑊 )
335 333 334 syl ( 𝜑𝑋 ∈ dom 𝑊 )