This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( 𝜑 → ( 𝑎 ∈ 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 biimtrid ⊢ ( 𝜑 → ( 𝑠 ∈ 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 biimtrrid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛 ∩ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑛 ∧ 𝑏 𝑊 𝑡 ) ) → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) 𝑧 𝑠 𝑣 ) )
132 131 expr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛 ∩ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤 ∈ 𝑛 ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) 𝑧 𝑠 𝑣 ) ) )
133 132 exlimdv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛 ∩ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤 ∈ 𝑛 ) → ( ∃ 𝑏 𝑏 𝑊 𝑡 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) 𝑧 𝑠 𝑣 ) ) )
134 71 133 biimtrid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛 ∩ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤 ∈ 𝑛 ) → ( 𝑡 ∈ ran 𝑊 → ( ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) 𝑧 𝑠 𝑣 ) ) )
135 134 rexlimdv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛 ∩ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤 ∈ 𝑛 ) → ( ∃ 𝑡 ∈ ran 𝑊 ⟨ 𝑤 , 𝑣 ⟩ ∈ 𝑡 → ∃ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) 𝑧 𝑠 𝑣 ) )
136 69 135 biimtrid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑣 ∈ ( 𝑛 ∩ 𝑎 ) ∧ ∀ 𝑧 ∈ ( 𝑛 ∩ 𝑎 ) ¬ 𝑧 𝑠 𝑣 ) ) ∧ 𝑤 ∈ 𝑛 ) → ( 𝑤 ∪ 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 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) → ( 𝑎 ∈ dom 𝑊 → ( 𝑦 ∈ 𝑎 → ∃ 𝑣 ∈ 𝑛 ∀ 𝑤 ∈ 𝑛 ¬ 𝑤 ∪ ran 𝑊 𝑣 ) ) )
143 142 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) → ( ∃ 𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → ∃ 𝑣 ∈ 𝑛 ∀ 𝑤 ∈ 𝑛 ¬ 𝑤 ∪ ran 𝑊 𝑣 ) )
144 46 143 mpd ⊢ ( ( 𝜑 ∧ ( 𝑛 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑛 ) ) → ∃ 𝑣 ∈ 𝑛 ∀ 𝑤 ∈ 𝑛 ¬ 𝑤 ∪ ran 𝑊 𝑣 )
145 144 expr ⊢ ( ( 𝜑 ∧ 𝑛 ⊆ 𝑋 ) → ( 𝑦 ∈ 𝑛 → ∃ 𝑣 ∈ 𝑛 ∀ 𝑤 ∈ 𝑛 ¬ 𝑤 ∪ ran 𝑊 𝑣 ) )
146 145 exlimdv ⊢ ( ( 𝜑 ∧ 𝑛 ⊆ 𝑋 ) → ( ∃ 𝑦 𝑦 ∈ 𝑛 → ∃ 𝑣 ∈ 𝑛 ∀ 𝑤 ∈ 𝑛 ¬ 𝑤 ∪ ran 𝑊 𝑣 ) )
147 40 146 biimtrid ⊢ ( ( 𝜑 ∧ 𝑛 ⊆ 𝑋 ) → ( 𝑛 ≠ ∅ → ∃ 𝑣 ∈ 𝑛 ∀ 𝑤 ∈ 𝑛 ¬ 𝑤 ∪ 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 biimtrid ⊢ ( 𝜑 → ( ( 𝑎 ∈ dom 𝑊 ∧ 𝑏 ∈ dom 𝑊 ) → ( ( 𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏 ) → ( 𝑦 ∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤 ∪ ran 𝑊 𝑦 ) ) ) )
209 208 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊 ∃ 𝑏 ∈ dom 𝑊 ( 𝑦 ∈ 𝑎 ∧ 𝑤 ∈ 𝑏 ) → ( 𝑦 ∪ ran 𝑊 𝑤 ∨ 𝑦 = 𝑤 ∨ 𝑤 ∪ ran 𝑊 𝑦 ) ) )
210 157 209 biimtrid ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑦 ∪ 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 imbitrrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑎 ⊆ 𝑏 ∧ 𝑠 = ( 𝑡 ∩ ( 𝑏 × 𝑎 ) ) ) ) → ( 𝑧 𝑡 𝑤 → 𝑧 ( 𝑏 × 𝑎 ) 𝑤 ) )
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 biimtrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑏 𝑊 𝑡 ) ) ∧ ( ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ∧ 𝑦 ∈ 𝑎 ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) )
266 265 exp32 ⊢ ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑏 𝑊 𝑡 ) ) → ( ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) → ( 𝑦 ∈ 𝑎 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) ) )
267 266 expr ⊢ ( ( 𝜑 ∧ 𝑎 𝑊 𝑠 ) → ( 𝑏 𝑊 𝑡 → ( ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) → ( 𝑦 ∈ 𝑎 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) ) ) )
268 267 com24 ⊢ ( ( 𝜑 ∧ 𝑎 𝑊 𝑠 ) → ( 𝑦 ∈ 𝑎 → ( ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) ) ) )
269 268 impr ⊢ ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) → ( ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) ) )
270 269 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ) → ( 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) )
271 270 exlimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ) → ( ∃ 𝑏 𝑏 𝑊 𝑡 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) )
272 71 271 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ) → ( 𝑡 ∈ ran 𝑊 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) ) )
273 272 rexlimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ) → ( ∃ 𝑡 ∈ ran 𝑊 ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑡 → 𝑧 𝑠 𝑤 ) )
274 231 273 biimtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 𝑊 𝑠 ∧ 𝑦 ∈ 𝑎 ) ) ∧ ( 𝑤 𝑠 𝑦 ∨ 𝑤 = 𝑦 ) ) → ( 𝑧 ∪ 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 biimtrid ⊢ ( 𝜑 → ( 𝑎 ∈ dom 𝑊 → ( 𝑦 ∈ 𝑎 → [ ( ◡ ∪ ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ∪ ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
328 327 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ dom 𝑊 𝑦 ∈ 𝑎 → [ ( ◡ ∪ ran 𝑊 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( ∪ ran 𝑊 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
329 45 328 biimtrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 → [ ( ◡ ∪ 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 𝑊 )