Metamath Proof Explorer

Theorem neibastop2lem

Description: Lemma for neibastop2 . (Contributed by Jeff Hankins, 12-Sep-2009)

Ref Expression
Hypotheses neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
neibastop1.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
neibastop1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
neibastop2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
neibastop2.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝑋 )
neibastop2.f ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐹 ‘ 𝑃 ) )
neibastop2.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝑁 )
neibastop2.g ⊢ 𝐺 = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω )
neibastop2.s ⊢ 𝑆 = { 𝑦 ∈ 𝑋 ∣ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ }
Assertion neibastop2lem ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 neibastop1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 neibastop1.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
3 neibastop1.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 ( 𝑣 ∩ 𝑤 ) ) ≠ ∅ )
4 neibastop1.4 ⊢ 𝐽 = { 𝑜 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ }
5 neibastop1.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝑣 )
6 neibastop1.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
7 neibastop2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
8 neibastop2.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝑋 )
9 neibastop2.f ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐹 ‘ 𝑃 ) )
10 neibastop2.u ⊢ ( 𝜑 → 𝑈 ⊆ 𝑁 )
11 neibastop2.g ⊢ 𝐺 = ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω )
12 neibastop2.s ⊢ 𝑆 = { 𝑦 ∈ 𝑋 ∣ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ }
13 ssrab2 ⊢ { 𝑦 ∈ 𝑋 ∣ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ } ⊆ 𝑋
14 12 13 eqsstri ⊢ 𝑆 ⊆ 𝑋
15 elpw2g ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
16 1 15 syl ⊢ ( 𝜑 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
17 14 16 mpbiri ⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝑋 )
18 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
19 18 ineq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) )
20 19 neeq1d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
21 20 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
22 21 12 elrab2 ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
23 frfnom ⊢ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω ) Fn ω
24 11 fneq1i ⊢ ( 𝐺 Fn ω ↔ ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω ) Fn ω )
25 23 24 mpbir ⊢ 𝐺 Fn ω
26 fnunirn ⊢ ( 𝐺 Fn ω → ( 𝑓 ∈ ∪ ran 𝐺 ↔ ∃ 𝑘 ∈ ω 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) )
27 25 26 ax-mp ⊢ ( 𝑓 ∈ ∪ ran 𝐺 ↔ ∃ 𝑘 ∈ ω 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) )
28 n0 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) )
29 inss1 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ⊆ ( 𝐹 ‘ 𝑥 )
30 29 sseli ⊢ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) → 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) )
31 6 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
32 30 31 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
33 32 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ∃ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
34 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) )
35 fvssunirn ⊢ ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ran 𝐹
36 2 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝒫 𝒫 𝑋 ∖ { ∅ } ) )
37 36 difss2d ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋 )
38 sspwuni ⊢ ( ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ↔ ∪ ran 𝐹 ⊆ 𝒫 𝑋 )
39 37 38 sylib ⊢ ( 𝜑 → ∪ ran 𝐹 ⊆ 𝒫 𝑋 )
40 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ∪ ran 𝐹 ⊆ 𝒫 𝑋 )
41 35 40 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ 𝒫 𝑋 )
42 41 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑡 ∈ 𝒫 𝑋 )
43 42 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑡 ⊆ 𝑋 )
44 43 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑡 ) → 𝑦 ∈ 𝑋 )
45 44 adantrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑡 ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → 𝑦 ∈ 𝑋 )
46 simprlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) )
47 rspe ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) → ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) )
48 47 ad2ant2l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) )
49 eliun ⊢ ( 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
50 pweq ⊢ ( 𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓 )
51 50 ineq2d ⊢ ( 𝑧 = 𝑓 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) )
52 51 eleq2d ⊢ ( 𝑧 = 𝑓 → ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ↔ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) )
53 52 rexbidv ⊢ ( 𝑧 = 𝑓 → ( ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) )
54 49 53 bitrid ⊢ ( 𝑧 = 𝑓 → ( 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ↔ ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) )
55 54 rspcev ⊢ ( ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ∃ 𝑥 ∈ 𝑋 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) → ∃ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
56 46 48 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ∃ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
57 eliun ⊢ ( 𝑣 ∈ ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ↔ ∃ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) 𝑣 ∈ ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
58 56 57 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → 𝑣 ∈ ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
59 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → 𝜑 )
60 simprll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → 𝑘 ∈ ω )
61 fvssunirn ⊢ ( 𝐺 ‘ 𝑘 ) ⊆ ∪ ran 𝐺
62 fveq2 ⊢ ( 𝑛 = ∅ → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ∅ ) )
63 11 fveq1i ⊢ ( 𝐺 ‘ ∅ ) = ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω ) ‘ ∅ )
64 snex ⊢ { 𝑈 } ∈ V
65 fr0g ⊢ ( { 𝑈 } ∈ V → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω ) ‘ ∅ ) = { 𝑈 } )
66 64 65 ax-mp ⊢ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ) , { 𝑈 } ) ↾ ω ) ‘ ∅ ) = { 𝑈 }
67 63 66 eqtri ⊢ ( 𝐺 ‘ ∅ ) = { 𝑈 }
68 62 67 eqtrdi ⊢ ( 𝑛 = ∅ → ( 𝐺 ‘ 𝑛 ) = { 𝑈 } )
69 68 sseq1d ⊢ ( 𝑛 = ∅ → ( ( 𝐺 ‘ 𝑛 ) ⊆ 𝒫 𝑈 ↔ { 𝑈 } ⊆ 𝒫 𝑈 ) )
70 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
71 70 sseq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐺 ‘ 𝑛 ) ⊆ 𝒫 𝑈 ↔ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) )
72 fveq2 ⊢ ( 𝑛 = suc 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ suc 𝑘 ) )
73 72 sseq1d ⊢ ( 𝑛 = suc 𝑘 → ( ( 𝐺 ‘ 𝑛 ) ⊆ 𝒫 𝑈 ↔ ( 𝐺 ‘ suc 𝑘 ) ⊆ 𝒫 𝑈 ) )
74 pwidg ⊢ ( 𝑈 ∈ ( 𝐹 ‘ 𝑃 ) → 𝑈 ∈ 𝒫 𝑈 )
75 9 74 syl ⊢ ( 𝜑 → 𝑈 ∈ 𝒫 𝑈 )
76 75 snssd ⊢ ( 𝜑 → { 𝑈 } ⊆ 𝒫 𝑈 )
77 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → 𝑘 ∈ ω )
78 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → 𝑈 ∈ ( 𝐹 ‘ 𝑃 ) )
79 78 pwexd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → 𝒫 𝑈 ∈ V )
80 inss2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑧
81 elpwi ⊢ ( 𝑧 ∈ 𝒫 𝑈 → 𝑧 ⊆ 𝑈 )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝑈 ) → 𝑧 ⊆ 𝑈 )
83 82 sspwd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝑈 ) → 𝒫 𝑧 ⊆ 𝒫 𝑈 )
84 80 83 sstrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝑈 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
85 84 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝑈 ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
86 iunss ⊢ ( ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
87 85 86 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝒫 𝑈 ) → ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
88 87 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝒫 𝑈 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
89 ssralv ⊢ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 → ( ∀ 𝑧 ∈ 𝒫 𝑈 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 → ∀ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 ) )
90 89 adantl ⊢ ( ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) → ( ∀ 𝑧 ∈ 𝒫 𝑈 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 → ∀ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 ) )
91 88 90 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → ∀ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
92 iunss ⊢ ( ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 ↔ ∀ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
93 91 92 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ⊆ 𝒫 𝑈 )
94 79 93 ssexd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ∈ V )
95 iuneq1 ⊢ ( 𝑦 = 𝑎 → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
96 iuneq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑘 ) → ∪ 𝑧 ∈ 𝑦 ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) = ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
97 11 95 96 frsucmpt2 ⊢ ( ( 𝑘 ∈ ω ∧ ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) ∈ V ) → ( 𝐺 ‘ suc 𝑘 ) = ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
98 77 94 97 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → ( 𝐺 ‘ suc 𝑘 ) = ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
99 98 93 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ω ∧ ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 ) ) → ( 𝐺 ‘ suc 𝑘 ) ⊆ 𝒫 𝑈 )
100 99 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ) → ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 → ( 𝐺 ‘ suc 𝑘 ) ⊆ 𝒫 𝑈 ) )
101 100 expcom ⊢ ( 𝑘 ∈ ω → ( 𝜑 → ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 → ( 𝐺 ‘ suc 𝑘 ) ⊆ 𝒫 𝑈 ) ) )
102 69 71 73 76 101 finds2 ⊢ ( 𝑛 ∈ ω → ( 𝜑 → ( 𝐺 ‘ 𝑛 ) ⊆ 𝒫 𝑈 ) )
103 fvex ⊢ ( 𝐺 ‘ 𝑛 ) ∈ V
104 103 elpw ⊢ ( ( 𝐺 ‘ 𝑛 ) ∈ 𝒫 𝒫 𝑈 ↔ ( 𝐺 ‘ 𝑛 ) ⊆ 𝒫 𝑈 )
105 102 104 imbitrrdi ⊢ ( 𝑛 ∈ ω → ( 𝜑 → ( 𝐺 ‘ 𝑛 ) ∈ 𝒫 𝒫 𝑈 ) )
106 105 com12 ⊢ ( 𝜑 → ( 𝑛 ∈ ω → ( 𝐺 ‘ 𝑛 ) ∈ 𝒫 𝒫 𝑈 ) )
107 106 ralrimiv ⊢ ( 𝜑 → ∀ 𝑛 ∈ ω ( 𝐺 ‘ 𝑛 ) ∈ 𝒫 𝒫 𝑈 )
108 ffnfv ⊢ ( 𝐺 : ω ⟶ 𝒫 𝒫 𝑈 ↔ ( 𝐺 Fn ω ∧ ∀ 𝑛 ∈ ω ( 𝐺 ‘ 𝑛 ) ∈ 𝒫 𝒫 𝑈 ) )
109 25 108 mpbiran ⊢ ( 𝐺 : ω ⟶ 𝒫 𝒫 𝑈 ↔ ∀ 𝑛 ∈ ω ( 𝐺 ‘ 𝑛 ) ∈ 𝒫 𝒫 𝑈 )
110 107 109 sylibr ⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝒫 𝒫 𝑈 )
111 110 frnd ⊢ ( 𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈 )
112 sspwuni ⊢ ( ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ↔ ∪ ran 𝐺 ⊆ 𝒫 𝑈 )
113 111 112 sylib ⊢ ( 𝜑 → ∪ ran 𝐺 ⊆ 𝒫 𝑈 )
114 113 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ∪ ran 𝐺 ⊆ 𝒫 𝑈 )
115 61 114 sstrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 )
116 59 60 115 98 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ( 𝐺 ‘ suc 𝑘 ) = ∪ 𝑧 ∈ ( 𝐺 ‘ 𝑘 ) ∪ 𝑥 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑧 ) )
117 58 116 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → 𝑣 ∈ ( 𝐺 ‘ suc 𝑘 ) )
118 peano2 ⊢ ( 𝑘 ∈ ω → suc 𝑘 ∈ ω )
119 60 118 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → suc 𝑘 ∈ ω )
120 fnfvelrn ⊢ ( ( 𝐺 Fn ω ∧ suc 𝑘 ∈ ω ) → ( 𝐺 ‘ suc 𝑘 ) ∈ ran 𝐺 )
121 25 119 120 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ( 𝐺 ‘ suc 𝑘 ) ∈ ran 𝐺 )
122 elunii ⊢ ( ( 𝑣 ∈ ( 𝐺 ‘ suc 𝑘 ) ∧ ( 𝐺 ‘ suc 𝑘 ) ∈ ran 𝐺 ) → 𝑣 ∈ ∪ ran 𝐺 )
123 117 121 122 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → 𝑣 ∈ ∪ ran 𝐺 )
124 123 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑡 ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → 𝑣 ∈ ∪ ran 𝐺 )
125 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑡 ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ )
126 pweq ⊢ ( 𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣 )
127 126 ineq2d ⊢ ( 𝑓 = 𝑣 → ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) = ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) )
128 127 neeq1d ⊢ ( 𝑓 = 𝑣 → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) )
129 128 rspcev ⊢ ( ( 𝑣 ∈ ∪ ran 𝐺 ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) → ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ )
130 124 125 129 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑡 ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ )
131 12 reqabi ⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
132 45 130 131 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑡 ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → 𝑦 ∈ 𝑆 )
133 132 expr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑡 ) → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ → 𝑦 ∈ 𝑆 ) )
134 133 ralimdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ → ∀ 𝑦 ∈ 𝑡 𝑦 ∈ 𝑆 ) )
135 134 impr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → ∀ 𝑦 ∈ 𝑡 𝑦 ∈ 𝑆 )
136 dfss3 ⊢ ( 𝑡 ⊆ 𝑆 ↔ ∀ 𝑦 ∈ 𝑡 𝑦 ∈ 𝑆 )
137 135 136 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → 𝑡 ⊆ 𝑆 )
138 velpw ⊢ ( 𝑡 ∈ 𝒫 𝑆 ↔ 𝑡 ⊆ 𝑆 )
139 137 138 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → 𝑡 ∈ 𝒫 𝑆 )
140 inelcm ⊢ ( ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑡 ∈ 𝒫 𝑆 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ )
141 34 139 140 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑡 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑣 ) ≠ ∅ ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ )
142 33 141 rexlimddv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ∧ 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ )
143 142 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ) → ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
144 143 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ) → ( ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
145 28 144 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑘 ∈ ω ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
146 145 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑘 ∈ ω 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) ) )
147 27 146 biimtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑓 ∈ ∪ ran 𝐺 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) ) )
148 147 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
149 148 expimpd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
150 22 149 biimtrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
151 150 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ )
152 pweq ⊢ ( 𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆 )
153 152 ineq2d ⊢ ( 𝑜 = 𝑆 → ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) = ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) )
154 153 neeq1d ⊢ ( 𝑜 = 𝑆 → ( ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
155 154 raleqbi1dv ⊢ ( 𝑜 = 𝑆 → ( ∀ 𝑥 ∈ 𝑜 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑜 ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝑆 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
156 155 4 elrab2 ⊢ ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝐹 ‘ 𝑥 ) ∩ 𝒫 𝑆 ) ≠ ∅ ) )
157 17 151 156 sylanbrc ⊢ ( 𝜑 → 𝑆 ∈ 𝐽 )
158 snidg ⊢ ( 𝑈 ∈ ( 𝐹 ‘ 𝑃 ) → 𝑈 ∈ { 𝑈 } )
159 9 158 syl ⊢ ( 𝜑 → 𝑈 ∈ { 𝑈 } )
160 peano1 ⊢ ∅ ∈ ω
161 fnfvelrn ⊢ ( ( 𝐺 Fn ω ∧ ∅ ∈ ω ) → ( 𝐺 ‘ ∅ ) ∈ ran 𝐺 )
162 25 160 161 mp2an ⊢ ( 𝐺 ‘ ∅ ) ∈ ran 𝐺
163 67 162 eqeltrri ⊢ { 𝑈 } ∈ ran 𝐺
164 elunii ⊢ ( ( 𝑈 ∈ { 𝑈 } ∧ { 𝑈 } ∈ ran 𝐺 ) → 𝑈 ∈ ∪ ran 𝐺 )
165 159 163 164 sylancl ⊢ ( 𝜑 → 𝑈 ∈ ∪ ran 𝐺 )
166 inelcm ⊢ ( ( 𝑈 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑈 ∈ 𝒫 𝑈 ) → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑈 ) ≠ ∅ )
167 9 75 166 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑈 ) ≠ ∅ )
168 pweq ⊢ ( 𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈 )
169 168 ineq2d ⊢ ( 𝑓 = 𝑈 → ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) = ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑈 ) )
170 169 neeq1d ⊢ ( 𝑓 = 𝑈 → ( ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑈 ) ≠ ∅ ) )
171 170 rspcev ⊢ ( ( 𝑈 ∈ ∪ ran 𝐺 ∧ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑈 ) ≠ ∅ ) → ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) ≠ ∅ )
172 165 167 171 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) ≠ ∅ )
173 fveq2 ⊢ ( 𝑦 = 𝑃 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑃 ) )
174 173 ineq1d ⊢ ( 𝑦 = 𝑃 → ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) = ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) )
175 174 neeq1d ⊢ ( 𝑦 = 𝑃 → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
176 175 rexbidv ⊢ ( 𝑦 = 𝑃 → ( ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
177 176 12 elrab2 ⊢ ( 𝑃 ∈ 𝑆 ↔ ( 𝑃 ∈ 𝑋 ∧ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑃 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) )
178 7 172 177 sylanbrc ⊢ ( 𝜑 → 𝑃 ∈ 𝑆 )
179 eluni2 ⊢ ( 𝑓 ∈ ∪ ran 𝐺 ↔ ∃ 𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 )
180 eleq2 ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑘 ) → ( 𝑓 ∈ 𝑧 ↔ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) )
181 180 rexrn ⊢ ( 𝐺 Fn ω → ( ∃ 𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃ 𝑘 ∈ ω 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) )
182 25 181 ax-mp ⊢ ( ∃ 𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ ∃ 𝑘 ∈ ω 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) )
183 110 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝐺 : ω ⟶ 𝒫 𝒫 𝑈 )
184 183 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝒫 𝒫 𝑈 )
185 184 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) → ( 𝐺 ‘ 𝑘 ) ⊆ 𝒫 𝑈 )
186 185 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) → 𝑓 ∈ 𝒫 𝑈 )
187 186 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) ) → 𝑓 ∈ 𝒫 𝑈 )
188 187 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) ) → 𝑓 ⊆ 𝑈 )
189 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) ) → 𝑈 ⊆ 𝑁 )
190 188 189 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) ) → 𝑓 ⊆ 𝑁 )
191 n0 ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) )
192 elin ⊢ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ↔ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) )
193 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → 𝑣 ∈ 𝒫 𝑓 )
194 193 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → 𝑣 ⊆ 𝑓 )
195 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → 𝑦 ∈ 𝑋 )
196 5 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑥 ∈ 𝑣 ) )
197 196 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑥 ∈ 𝑣 ) )
198 197 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑥 ∈ 𝑣 ) )
199 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) )
200 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
201 200 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ) )
202 elequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣 ) )
203 201 202 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑥 ∈ 𝑣 ) ↔ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) → 𝑦 ∈ 𝑣 ) ) )
204 203 rspcv ⊢ ( 𝑦 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑣 ∈ ( 𝐹 ‘ 𝑥 ) → 𝑥 ∈ 𝑣 ) → ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) → 𝑦 ∈ 𝑣 ) ) )
205 195 198 199 204 syl3c ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → 𝑦 ∈ 𝑣 )
206 194 205 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) ) ) → 𝑦 ∈ 𝑓 )
207 206 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) → ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑣 ∈ 𝒫 𝑓 ) → 𝑦 ∈ 𝑓 ) )
208 192 207 biimtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) → ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) → 𝑦 ∈ 𝑓 ) )
209 208 exlimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) → ( ∃ 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) → 𝑦 ∈ 𝑓 ) )
210 191 209 biimtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ → 𝑦 ∈ 𝑓 ) )
211 210 impr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) ) → 𝑦 ∈ 𝑓 )
212 190 211 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) ∧ ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) ) → 𝑦 ∈ 𝑁 )
213 212 exp32 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑘 ∈ ω ) → ( 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ → 𝑦 ∈ 𝑁 ) ) )
214 213 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑘 ∈ ω 𝑓 ∈ ( 𝐺 ‘ 𝑘 ) → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ → 𝑦 ∈ 𝑁 ) ) )
215 182 214 biimtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ran 𝐺 𝑓 ∈ 𝑧 → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ → 𝑦 ∈ 𝑁 ) ) )
216 179 215 biimtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑓 ∈ ∪ ran 𝐺 → ( ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ → 𝑦 ∈ 𝑁 ) ) )
217 216 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ → 𝑦 ∈ 𝑁 ) )
218 217 3impia ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ∧ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ ) → 𝑦 ∈ 𝑁 )
219 218 rabssdv ⊢ ( 𝜑 → { 𝑦 ∈ 𝑋 ∣ ∃ 𝑓 ∈ ∪ ran 𝐺 ( ( 𝐹 ‘ 𝑦 ) ∩ 𝒫 𝑓 ) ≠ ∅ } ⊆ 𝑁 )
220 12 219 eqsstrid ⊢ ( 𝜑 → 𝑆 ⊆ 𝑁 )
221 eleq2 ⊢ ( 𝑢 = 𝑆 → ( 𝑃 ∈ 𝑢 ↔ 𝑃 ∈ 𝑆 ) )
222 sseq1 ⊢ ( 𝑢 = 𝑆 → ( 𝑢 ⊆ 𝑁 ↔ 𝑆 ⊆ 𝑁 ) )
223 221 222 anbi12d ⊢ ( 𝑢 = 𝑆 → ( ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) ↔ ( 𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁 ) ) )
224 223 rspcev ⊢ ( ( 𝑆 ∈ 𝐽 ∧ ( 𝑃 ∈ 𝑆 ∧ 𝑆 ⊆ 𝑁 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) )
225 157 178 220 224 syl12anc ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁 ) )