Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  neibastop2lem Structured version   Visualization version   GIF version

Theorem neibastop2lem 34878
Description: Lemma for neibastop2 34879. (Contributed by Jeff Hankins, 12-Sep-2009.)
Hypotheses
Ref Expression
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
Ref Expression
neibastop2lem (πœ‘ β†’ βˆƒπ‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 ∧ 𝑒 βŠ† 𝑁))
Distinct variable groups:   𝑑,𝑓,𝑣,𝑦,𝑧,𝐺   𝑣,𝑒,π‘₯,𝑦,𝑧,𝐽   𝑓,π‘œ,𝑒,𝑀,π‘₯,𝑃,𝑑,𝑣,𝑦,𝑧   𝑓,𝑁,π‘œ,𝑑,𝑒,𝑣,𝑀,π‘₯,𝑦,𝑧   𝑆,𝑓,π‘œ,𝑑,𝑒,𝑣,π‘₯,𝑦   π‘ˆ,𝑓,π‘₯,𝑦,𝑧   𝑓,π‘Ž,π‘œ,𝑑,𝑒,𝑣,𝑀,π‘₯,𝑦,𝑧,𝐹   πœ‘,𝑓,π‘œ,𝑑,𝑣,𝑀,π‘₯,𝑦,𝑧   𝑋,π‘Ž,𝑓,π‘œ,𝑑,𝑒,𝑣,𝑀,π‘₯,𝑦,𝑧
Allowed substitution hints:   πœ‘(𝑒,π‘Ž)   𝑃(π‘Ž)   𝑆(𝑧,𝑀,π‘Ž)   π‘ˆ(𝑀,𝑣,𝑒,𝑑,π‘œ,π‘Ž)   𝐺(π‘₯,𝑀,𝑒,π‘œ,π‘Ž)   𝐽(𝑀,𝑑,𝑓,π‘œ,π‘Ž)   𝑁(π‘Ž)   𝑉(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑒,𝑑,𝑓,π‘œ,π‘Ž)

Proof of Theorem neibastop2lem
Dummy variables π‘˜ 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neibastop2.s . . . . 5 𝑆 = {𝑦 ∈ 𝑋 ∣ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…}
2 ssrab2 4038 . . . . 5 {𝑦 ∈ 𝑋 ∣ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…} βŠ† 𝑋
31, 2eqsstri 3979 . . . 4 𝑆 βŠ† 𝑋
4 neibastop1.1 . . . . 5 (πœ‘ β†’ 𝑋 ∈ 𝑉)
5 elpw2g 5302 . . . . 5 (𝑋 ∈ 𝑉 β†’ (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 βŠ† 𝑋))
64, 5syl 17 . . . 4 (πœ‘ β†’ (𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 βŠ† 𝑋))
73, 6mpbiri 258 . . 3 (πœ‘ β†’ 𝑆 ∈ 𝒫 𝑋)
8 fveq2 6843 . . . . . . . . 9 (𝑦 = π‘₯ β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘₯))
98ineq1d 4172 . . . . . . . 8 (𝑦 = π‘₯ β†’ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))
109neeq1d 3000 . . . . . . 7 (𝑦 = π‘₯ β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ…))
1110rexbidv 3172 . . . . . 6 (𝑦 = π‘₯ β†’ (βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… ↔ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ…))
1211, 1elrab2 3649 . . . . 5 (π‘₯ ∈ 𝑆 ↔ (π‘₯ ∈ 𝑋 ∧ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ…))
13 frfnom 8382 . . . . . . . . . 10 (rec((π‘Ž ∈ V ↦ βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)), {π‘ˆ}) β†Ύ Ο‰) Fn Ο‰
14 neibastop2.g . . . . . . . . . . 11 𝐺 = (rec((π‘Ž ∈ V ↦ βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)), {π‘ˆ}) β†Ύ Ο‰)
1514fneq1i 6600 . . . . . . . . . 10 (𝐺 Fn Ο‰ ↔ (rec((π‘Ž ∈ V ↦ βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)), {π‘ˆ}) β†Ύ Ο‰) Fn Ο‰)
1613, 15mpbir 230 . . . . . . . . 9 𝐺 Fn Ο‰
17 fnunirn 7202 . . . . . . . . 9 (𝐺 Fn Ο‰ β†’ (𝑓 ∈ βˆͺ ran 𝐺 ↔ βˆƒπ‘˜ ∈ Ο‰ 𝑓 ∈ (πΊβ€˜π‘˜)))
1816, 17ax-mp 5 . . . . . . . 8 (𝑓 ∈ βˆͺ ran 𝐺 ↔ βˆƒπ‘˜ ∈ Ο‰ 𝑓 ∈ (πΊβ€˜π‘˜))
19 n0 4307 . . . . . . . . . 10 (((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))
20 inss1 4189 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) βŠ† (πΉβ€˜π‘₯)
2120sseli 3941 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β†’ 𝑣 ∈ (πΉβ€˜π‘₯))
22 neibastop1.6 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
2322anassrs 469 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ (πΉβ€˜π‘₯)) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
2421, 23sylan2 594 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓)) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
2524adantrl 715 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
26 simprl 770 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ (𝑑 ∈ (πΉβ€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ 𝑑 ∈ (πΉβ€˜π‘₯))
27 fvssunirn 6876 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πΉβ€˜π‘₯) βŠ† βˆͺ ran 𝐹
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝐹:π‘‹βŸΆ(𝒫 𝒫 𝑋 βˆ– {βˆ…}))
2928frnd 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ ran 𝐹 βŠ† (𝒫 𝒫 𝑋 βˆ– {βˆ…}))
3029difss2d 4095 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ran 𝐹 βŠ† 𝒫 𝒫 𝑋)
31 sspwuni 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝐹 βŠ† 𝒫 𝒫 𝑋 ↔ βˆͺ ran 𝐹 βŠ† 𝒫 𝑋)
3230, 31sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ βˆͺ ran 𝐹 βŠ† 𝒫 𝑋)
3332ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ βˆͺ ran 𝐹 βŠ† 𝒫 𝑋)
3427, 33sstrid 3956 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ (πΉβ€˜π‘₯) βŠ† 𝒫 𝑋)
3534sselda 3945 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) β†’ 𝑑 ∈ 𝒫 𝑋)
3635elpwid 4570 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) β†’ 𝑑 βŠ† 𝑋)
3736sselda 3945 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ 𝑦 ∈ 𝑑) β†’ 𝑦 ∈ 𝑋)
3837adantrr 716 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ (𝑦 ∈ 𝑑 ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ 𝑦 ∈ 𝑋)
39 simprlr 779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ 𝑓 ∈ (πΊβ€˜π‘˜))
40 rspe 3231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓)) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))
4140ad2ant2l 745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))
42 eliun 4959 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 ∈ βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ↔ βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
43 pweq 4575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑓 β†’ 𝒫 𝑧 = 𝒫 𝑓)
4443ineq2d 4173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑓 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))
4544eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑓 β†’ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓)))
4645rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑓 β†’ (βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ↔ βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓)))
4742, 46bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑓 β†’ (𝑣 ∈ βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ↔ βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓)))
4847rspcev 3580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (πΊβ€˜π‘˜) ∧ βˆƒπ‘₯ ∈ 𝑋 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓)) β†’ βˆƒπ‘§ ∈ (πΊβ€˜π‘˜)𝑣 ∈ βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
4939, 41, 48syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ βˆƒπ‘§ ∈ (πΊβ€˜π‘˜)𝑣 ∈ βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
50 eliun 4959 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 ∈ βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ↔ βˆƒπ‘§ ∈ (πΊβ€˜π‘˜)𝑣 ∈ βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
5149, 50sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ 𝑣 ∈ βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
52 simpll 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ πœ‘)
53 simprll 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ π‘˜ ∈ Ο‰)
54 fvssunirn 6876 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πΊβ€˜π‘˜) βŠ† βˆͺ ran 𝐺
55 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑛 = βˆ… β†’ (πΊβ€˜π‘›) = (πΊβ€˜βˆ…))
5614fveq1i 6844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (πΊβ€˜βˆ…) = ((rec((π‘Ž ∈ V ↦ βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)), {π‘ˆ}) β†Ύ Ο‰)β€˜βˆ…)
57 snex 5389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {π‘ˆ} ∈ V
58 fr0g 8383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ({π‘ˆ} ∈ V β†’ ((rec((π‘Ž ∈ V ↦ βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)), {π‘ˆ}) β†Ύ Ο‰)β€˜βˆ…) = {π‘ˆ})
5957, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((rec((π‘Ž ∈ V ↦ βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧)), {π‘ˆ}) β†Ύ Ο‰)β€˜βˆ…) = {π‘ˆ}
6056, 59eqtri 2761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (πΊβ€˜βˆ…) = {π‘ˆ}
6155, 60eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = βˆ… β†’ (πΊβ€˜π‘›) = {π‘ˆ})
6261sseq1d 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = βˆ… β†’ ((πΊβ€˜π‘›) βŠ† 𝒫 π‘ˆ ↔ {π‘ˆ} βŠ† 𝒫 π‘ˆ))
63 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = π‘˜ β†’ (πΊβ€˜π‘›) = (πΊβ€˜π‘˜))
6463sseq1d 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = π‘˜ β†’ ((πΊβ€˜π‘›) βŠ† 𝒫 π‘ˆ ↔ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ))
65 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = suc π‘˜ β†’ (πΊβ€˜π‘›) = (πΊβ€˜suc π‘˜))
6665sseq1d 3976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = suc π‘˜ β†’ ((πΊβ€˜π‘›) βŠ† 𝒫 π‘ˆ ↔ (πΊβ€˜suc π‘˜) βŠ† 𝒫 π‘ˆ))
67 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (πœ‘ β†’ π‘ˆ ∈ (πΉβ€˜π‘ƒ))
68 pwidg 4581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (π‘ˆ ∈ (πΉβ€˜π‘ƒ) β†’ π‘ˆ ∈ 𝒫 π‘ˆ)
6967, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (πœ‘ β†’ π‘ˆ ∈ 𝒫 π‘ˆ)
7069snssd 4770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (πœ‘ β†’ {π‘ˆ} βŠ† 𝒫 π‘ˆ)
71 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ π‘˜ ∈ Ο‰)
7267adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ π‘ˆ ∈ (πΉβ€˜π‘ƒ))
7372pwexd 5335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ 𝒫 π‘ˆ ∈ V)
74 inss2 4190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 𝑧
75 elpwi 4568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑧 ∈ 𝒫 π‘ˆ β†’ 𝑧 βŠ† π‘ˆ)
7675adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((πœ‘ ∧ 𝑧 ∈ 𝒫 π‘ˆ) β†’ 𝑧 βŠ† π‘ˆ)
7776sspwd 4574 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((πœ‘ ∧ 𝑧 ∈ 𝒫 π‘ˆ) β†’ 𝒫 𝑧 βŠ† 𝒫 π‘ˆ)
7874, 77sstrid 3956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((πœ‘ ∧ 𝑧 ∈ 𝒫 π‘ˆ) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
7978ralrimivw 3144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((πœ‘ ∧ 𝑧 ∈ 𝒫 π‘ˆ) β†’ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
80 iunss 5006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ ↔ βˆ€π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
8179, 80sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((πœ‘ ∧ 𝑧 ∈ 𝒫 π‘ˆ) β†’ βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
8281ralrimiva 3140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (πœ‘ β†’ βˆ€π‘§ ∈ 𝒫 π‘ˆβˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
83 ssralv 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ β†’ (βˆ€π‘§ ∈ 𝒫 π‘ˆβˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ β†’ βˆ€π‘§ ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ))
8483adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ) β†’ (βˆ€π‘§ ∈ 𝒫 π‘ˆβˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ β†’ βˆ€π‘§ ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ))
8582, 84mpan9 508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ βˆ€π‘§ ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
86 iunss 5006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ ↔ βˆ€π‘§ ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
8785, 86sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) βŠ† 𝒫 π‘ˆ)
8873, 87ssexd 5282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ∈ V)
89 iuneq1 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = π‘Ž β†’ βˆͺ 𝑧 ∈ 𝑦 βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) = βˆͺ 𝑧 ∈ π‘Ž βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
90 iuneq1 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = (πΊβ€˜π‘˜) β†’ βˆͺ 𝑧 ∈ 𝑦 βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) = βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
9114, 89, 90frsucmpt2 8387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((π‘˜ ∈ Ο‰ ∧ βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧) ∈ V) β†’ (πΊβ€˜suc π‘˜) = βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
9271, 88, 91syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ (πΊβ€˜suc π‘˜) = βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
9392, 87eqsstrd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)) β†’ (πΊβ€˜suc π‘˜) βŠ† 𝒫 π‘ˆ)
9493expr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((πœ‘ ∧ π‘˜ ∈ Ο‰) β†’ ((πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ β†’ (πΊβ€˜suc π‘˜) βŠ† 𝒫 π‘ˆ))
9594expcom 415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (π‘˜ ∈ Ο‰ β†’ (πœ‘ β†’ ((πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ β†’ (πΊβ€˜suc π‘˜) βŠ† 𝒫 π‘ˆ)))
9662, 64, 66, 70, 95finds2 7838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ Ο‰ β†’ (πœ‘ β†’ (πΊβ€˜π‘›) βŠ† 𝒫 π‘ˆ))
97 fvex 6856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (πΊβ€˜π‘›) ∈ V
9897elpw 4565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πΊβ€˜π‘›) ∈ 𝒫 𝒫 π‘ˆ ↔ (πΊβ€˜π‘›) βŠ† 𝒫 π‘ˆ)
9996, 98syl6ibr 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ Ο‰ β†’ (πœ‘ β†’ (πΊβ€˜π‘›) ∈ 𝒫 𝒫 π‘ˆ))
10099com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (πœ‘ β†’ (𝑛 ∈ Ο‰ β†’ (πΊβ€˜π‘›) ∈ 𝒫 𝒫 π‘ˆ))
101100ralrimiv 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ 𝒫 𝒫 π‘ˆ)
102 ffnfv 7067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐺:Ο‰βŸΆπ’« 𝒫 π‘ˆ ↔ (𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ 𝒫 𝒫 π‘ˆ))
10316, 102mpbiran 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺:Ο‰βŸΆπ’« 𝒫 π‘ˆ ↔ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ 𝒫 𝒫 π‘ˆ)
104101, 103sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝐺:Ο‰βŸΆπ’« 𝒫 π‘ˆ)
105104frnd 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ ran 𝐺 βŠ† 𝒫 𝒫 π‘ˆ)
106 sspwuni 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran 𝐺 βŠ† 𝒫 𝒫 π‘ˆ ↔ βˆͺ ran 𝐺 βŠ† 𝒫 π‘ˆ)
107105, 106sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ βˆͺ ran 𝐺 βŠ† 𝒫 π‘ˆ)
108107ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ βˆͺ ran 𝐺 βŠ† 𝒫 π‘ˆ)
10954, 108sstrid 3956 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)
11052, 53, 109, 92syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ (πΊβ€˜suc π‘˜) = βˆͺ 𝑧 ∈ (πΊβ€˜π‘˜)βˆͺ π‘₯ ∈ 𝑋 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑧))
11151, 110eleqtrrd 2837 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ 𝑣 ∈ (πΊβ€˜suc π‘˜))
112 peano2 7828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ Ο‰ β†’ suc π‘˜ ∈ Ο‰)
11353, 112syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ suc π‘˜ ∈ Ο‰)
114 fnfvelrn 7032 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn Ο‰ ∧ suc π‘˜ ∈ Ο‰) β†’ (πΊβ€˜suc π‘˜) ∈ ran 𝐺)
11516, 113, 114sylancr 588 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ (πΊβ€˜suc π‘˜) ∈ ran 𝐺)
116 elunii 4871 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ (πΊβ€˜suc π‘˜) ∧ (πΊβ€˜suc π‘˜) ∈ ran 𝐺) β†’ 𝑣 ∈ βˆͺ ran 𝐺)
117111, 115, 116syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ 𝑣 ∈ βˆͺ ran 𝐺)
118117ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ (𝑦 ∈ 𝑑 ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ 𝑣 ∈ βˆͺ ran 𝐺)
119 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ (𝑦 ∈ 𝑑 ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
120 pweq 4575 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑣 β†’ 𝒫 𝑓 = 𝒫 𝑣)
121120ineq2d 4173 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑣 β†’ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) = ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣))
122121neeq1d 3000 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑣 β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… ↔ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…))
123122rspcev 3580 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ∈ βˆͺ ran 𝐺 ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…) β†’ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)
124118, 119, 123syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ (𝑦 ∈ 𝑑 ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)
1251reqabi 3428 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ 𝑋 ∧ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…))
12638, 124, 125sylanbrc 584 . . . . . . . . . . . . . . . . . . 19 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ (𝑦 ∈ 𝑑 ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ 𝑦 ∈ 𝑆)
127126expr 458 . . . . . . . . . . . . . . . . . 18 (((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) ∧ 𝑦 ∈ 𝑑) β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ… β†’ 𝑦 ∈ 𝑆))
128127ralimdva 3161 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ 𝑑 ∈ (πΉβ€˜π‘₯)) β†’ (βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ… β†’ βˆ€π‘¦ ∈ 𝑑 𝑦 ∈ 𝑆))
129128impr 456 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ (𝑑 ∈ (πΉβ€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ βˆ€π‘¦ ∈ 𝑑 𝑦 ∈ 𝑆)
130 dfss3 3933 . . . . . . . . . . . . . . . 16 (𝑑 βŠ† 𝑆 ↔ βˆ€π‘¦ ∈ 𝑑 𝑦 ∈ 𝑆)
131129, 130sylibr 233 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ (𝑑 ∈ (πΉβ€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ 𝑑 βŠ† 𝑆)
132 velpw 4566 . . . . . . . . . . . . . . 15 (𝑑 ∈ 𝒫 𝑆 ↔ 𝑑 βŠ† 𝑆)
133131, 132sylibr 233 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ (𝑑 ∈ (πΉβ€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ 𝑑 ∈ 𝒫 𝑆)
134 inelcm 4425 . . . . . . . . . . . . . 14 ((𝑑 ∈ (πΉβ€˜π‘₯) ∧ 𝑑 ∈ 𝒫 𝑆) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…)
13526, 133, 134syl2anc 585 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) ∧ (𝑑 ∈ (πΉβ€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…)
13625, 135rexlimddv 3155 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ ((π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) ∧ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…)
137136expr 458 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜))) β†’ (𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
138137exlimdv 1937 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜))) β†’ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
13919, 138biimtrid 241 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ (π‘˜ ∈ Ο‰ ∧ 𝑓 ∈ (πΊβ€˜π‘˜))) β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ… β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
140139rexlimdvaa 3150 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (βˆƒπ‘˜ ∈ Ο‰ 𝑓 ∈ (πΊβ€˜π‘˜) β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ… β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…)))
14118, 140biimtrid 241 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑓 ∈ βˆͺ ran 𝐺 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ… β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…)))
142141rexlimdv 3147 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ… β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
143142expimpd 455 . . . . 5 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ∧ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘₯) ∩ 𝒫 𝑓) β‰  βˆ…) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
14412, 143biimtrid 241 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝑆 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
145144ralrimiv 3139 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑆 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…)
146 pweq 4575 . . . . . . 7 (π‘œ = 𝑆 β†’ 𝒫 π‘œ = 𝒫 𝑆)
147146ineq2d 4173 . . . . . 6 (π‘œ = 𝑆 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) = ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆))
148147neeq1d 3000 . . . . 5 (π‘œ = 𝑆 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
149148raleqbi1dv 3306 . . . 4 (π‘œ = 𝑆 β†’ (βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ… ↔ βˆ€π‘₯ ∈ 𝑆 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
150 neibastop1.4 . . . 4 𝐽 = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…}
151149, 150elrab2 3649 . . 3 (𝑆 ∈ 𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ βˆ€π‘₯ ∈ 𝑆 ((πΉβ€˜π‘₯) ∩ 𝒫 𝑆) β‰  βˆ…))
1527, 145, 151sylanbrc 584 . 2 (πœ‘ β†’ 𝑆 ∈ 𝐽)
153 neibastop2.p . . 3 (πœ‘ β†’ 𝑃 ∈ 𝑋)
154 snidg 4621 . . . . . 6 (π‘ˆ ∈ (πΉβ€˜π‘ƒ) β†’ π‘ˆ ∈ {π‘ˆ})
15567, 154syl 17 . . . . 5 (πœ‘ β†’ π‘ˆ ∈ {π‘ˆ})
156 peano1 7826 . . . . . . 7 βˆ… ∈ Ο‰
157 fnfvelrn 7032 . . . . . . 7 ((𝐺 Fn Ο‰ ∧ βˆ… ∈ Ο‰) β†’ (πΊβ€˜βˆ…) ∈ ran 𝐺)
15816, 156, 157mp2an 691 . . . . . 6 (πΊβ€˜βˆ…) ∈ ran 𝐺
15960, 158eqeltrri 2831 . . . . 5 {π‘ˆ} ∈ ran 𝐺
160 elunii 4871 . . . . 5 ((π‘ˆ ∈ {π‘ˆ} ∧ {π‘ˆ} ∈ ran 𝐺) β†’ π‘ˆ ∈ βˆͺ ran 𝐺)
161155, 159, 160sylancl 587 . . . 4 (πœ‘ β†’ π‘ˆ ∈ βˆͺ ran 𝐺)
162 inelcm 4425 . . . . 5 ((π‘ˆ ∈ (πΉβ€˜π‘ƒ) ∧ π‘ˆ ∈ 𝒫 π‘ˆ) β†’ ((πΉβ€˜π‘ƒ) ∩ 𝒫 π‘ˆ) β‰  βˆ…)
16367, 69, 162syl2anc 585 . . . 4 (πœ‘ β†’ ((πΉβ€˜π‘ƒ) ∩ 𝒫 π‘ˆ) β‰  βˆ…)
164 pweq 4575 . . . . . . 7 (𝑓 = π‘ˆ β†’ 𝒫 𝑓 = 𝒫 π‘ˆ)
165164ineq2d 4173 . . . . . 6 (𝑓 = π‘ˆ β†’ ((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) = ((πΉβ€˜π‘ƒ) ∩ 𝒫 π‘ˆ))
166165neeq1d 3000 . . . . 5 (𝑓 = π‘ˆ β†’ (((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) β‰  βˆ… ↔ ((πΉβ€˜π‘ƒ) ∩ 𝒫 π‘ˆ) β‰  βˆ…))
167166rspcev 3580 . . . 4 ((π‘ˆ ∈ βˆͺ ran 𝐺 ∧ ((πΉβ€˜π‘ƒ) ∩ 𝒫 π‘ˆ) β‰  βˆ…) β†’ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) β‰  βˆ…)
168161, 163, 167syl2anc 585 . . 3 (πœ‘ β†’ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) β‰  βˆ…)
169 fveq2 6843 . . . . . . 7 (𝑦 = 𝑃 β†’ (πΉβ€˜π‘¦) = (πΉβ€˜π‘ƒ))
170169ineq1d 4172 . . . . . 6 (𝑦 = 𝑃 β†’ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) = ((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓))
171170neeq1d 3000 . . . . 5 (𝑦 = 𝑃 β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… ↔ ((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) β‰  βˆ…))
172171rexbidv 3172 . . . 4 (𝑦 = 𝑃 β†’ (βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… ↔ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) β‰  βˆ…))
173172, 1elrab2 3649 . . 3 (𝑃 ∈ 𝑆 ↔ (𝑃 ∈ 𝑋 ∧ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘ƒ) ∩ 𝒫 𝑓) β‰  βˆ…))
174153, 168, 173sylanbrc 584 . 2 (πœ‘ β†’ 𝑃 ∈ 𝑆)
175 eluni2 4870 . . . . . . 7 (𝑓 ∈ βˆͺ ran 𝐺 ↔ βˆƒπ‘§ ∈ ran 𝐺 𝑓 ∈ 𝑧)
176 eleq2 2823 . . . . . . . . . 10 (𝑧 = (πΊβ€˜π‘˜) β†’ (𝑓 ∈ 𝑧 ↔ 𝑓 ∈ (πΊβ€˜π‘˜)))
177176rexrn 7038 . . . . . . . . 9 (𝐺 Fn Ο‰ β†’ (βˆƒπ‘§ ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ βˆƒπ‘˜ ∈ Ο‰ 𝑓 ∈ (πΊβ€˜π‘˜)))
17816, 177ax-mp 5 . . . . . . . 8 (βˆƒπ‘§ ∈ ran 𝐺 𝑓 ∈ 𝑧 ↔ βˆƒπ‘˜ ∈ Ο‰ 𝑓 ∈ (πΊβ€˜π‘˜))
179104adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑦 ∈ 𝑋) β†’ 𝐺:Ο‰βŸΆπ’« 𝒫 π‘ˆ)
180179ffvelcdmda 7036 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) β†’ (πΊβ€˜π‘˜) ∈ 𝒫 𝒫 π‘ˆ)
181180elpwid 4570 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) β†’ (πΊβ€˜π‘˜) βŠ† 𝒫 π‘ˆ)
182181sselda 3945 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) β†’ 𝑓 ∈ 𝒫 π‘ˆ)
183182adantrr 716 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)) β†’ 𝑓 ∈ 𝒫 π‘ˆ)
184183elpwid 4570 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)) β†’ 𝑓 βŠ† π‘ˆ)
185 neibastop2.u . . . . . . . . . . . . 13 (πœ‘ β†’ π‘ˆ βŠ† 𝑁)
186185ad3antrrr 729 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)) β†’ π‘ˆ βŠ† 𝑁)
187184, 186sstrd 3955 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)) β†’ 𝑓 βŠ† 𝑁)
188 n0 4307 . . . . . . . . . . . . 13 (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… ↔ βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓))
189 elin 3927 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))
190 simprrr 781 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ 𝑣 ∈ 𝒫 𝑓)
191190elpwid 4570 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ 𝑣 βŠ† 𝑓)
192 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ 𝑦 ∈ 𝑋)
193 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ π‘₯ ∈ 𝑣)
194193expr 458 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (𝑣 ∈ (πΉβ€˜π‘₯) β†’ π‘₯ ∈ 𝑣))
195194ralrimiva 3140 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (𝑣 ∈ (πΉβ€˜π‘₯) β†’ π‘₯ ∈ 𝑣))
196195ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ βˆ€π‘₯ ∈ 𝑋 (𝑣 ∈ (πΉβ€˜π‘₯) β†’ π‘₯ ∈ 𝑣))
197 simprrl 780 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ 𝑣 ∈ (πΉβ€˜π‘¦))
198 fveq2 6843 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑦 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘¦))
199198eleq2d 2820 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑦 β†’ (𝑣 ∈ (πΉβ€˜π‘₯) ↔ 𝑣 ∈ (πΉβ€˜π‘¦)))
200 elequ1 2114 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑦 β†’ (π‘₯ ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
201199, 200imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = 𝑦 β†’ ((𝑣 ∈ (πΉβ€˜π‘₯) β†’ π‘₯ ∈ 𝑣) ↔ (𝑣 ∈ (πΉβ€˜π‘¦) β†’ 𝑦 ∈ 𝑣)))
202201rspcv 3576 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 (𝑣 ∈ (πΉβ€˜π‘₯) β†’ π‘₯ ∈ 𝑣) β†’ (𝑣 ∈ (πΉβ€˜π‘¦) β†’ 𝑦 ∈ 𝑣)))
203192, 196, 197, 202syl3c 66 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ 𝑦 ∈ 𝑣)
204191, 203sseldd 3946 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ (𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓))) β†’ 𝑦 ∈ 𝑓)
205204expr 458 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) β†’ ((𝑣 ∈ (πΉβ€˜π‘¦) ∧ 𝑣 ∈ 𝒫 𝑓) β†’ 𝑦 ∈ 𝑓))
206189, 205biimtrid 241 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) β†’ (𝑣 ∈ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β†’ 𝑦 ∈ 𝑓))
207206exlimdv 1937 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) β†’ (βˆƒπ‘£ 𝑣 ∈ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β†’ 𝑦 ∈ 𝑓))
208188, 207biimtrid 241 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ 𝑓 ∈ (πΊβ€˜π‘˜)) β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… β†’ 𝑦 ∈ 𝑓))
209208impr 456 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)) β†’ 𝑦 ∈ 𝑓)
210187, 209sseldd 3946 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) ∧ (𝑓 ∈ (πΊβ€˜π‘˜) ∧ ((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…)) β†’ 𝑦 ∈ 𝑁)
211210exp32 422 . . . . . . . . 9 (((πœ‘ ∧ 𝑦 ∈ 𝑋) ∧ π‘˜ ∈ Ο‰) β†’ (𝑓 ∈ (πΊβ€˜π‘˜) β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… β†’ 𝑦 ∈ 𝑁)))
212211rexlimdva 3149 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ 𝑋) β†’ (βˆƒπ‘˜ ∈ Ο‰ 𝑓 ∈ (πΊβ€˜π‘˜) β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… β†’ 𝑦 ∈ 𝑁)))
213178, 212biimtrid 241 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ 𝑋) β†’ (βˆƒπ‘§ ∈ ran 𝐺 𝑓 ∈ 𝑧 β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… β†’ 𝑦 ∈ 𝑁)))
214175, 213biimtrid 241 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ 𝑋) β†’ (𝑓 ∈ βˆͺ ran 𝐺 β†’ (((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… β†’ 𝑦 ∈ 𝑁)))
215214rexlimdv 3147 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ 𝑋) β†’ (βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ… β†’ 𝑦 ∈ 𝑁))
2162153impia 1118 . . . 4 ((πœ‘ ∧ 𝑦 ∈ 𝑋 ∧ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…) β†’ 𝑦 ∈ 𝑁)
217216rabssdv 4033 . . 3 (πœ‘ β†’ {𝑦 ∈ 𝑋 ∣ βˆƒπ‘“ ∈ βˆͺ ran 𝐺((πΉβ€˜π‘¦) ∩ 𝒫 𝑓) β‰  βˆ…} βŠ† 𝑁)
2181, 217eqsstrid 3993 . 2 (πœ‘ β†’ 𝑆 βŠ† 𝑁)
219 eleq2 2823 . . . 4 (𝑒 = 𝑆 β†’ (𝑃 ∈ 𝑒 ↔ 𝑃 ∈ 𝑆))
220 sseq1 3970 . . . 4 (𝑒 = 𝑆 β†’ (𝑒 βŠ† 𝑁 ↔ 𝑆 βŠ† 𝑁))
221219, 220anbi12d 632 . . 3 (𝑒 = 𝑆 β†’ ((𝑃 ∈ 𝑒 ∧ 𝑒 βŠ† 𝑁) ↔ (𝑃 ∈ 𝑆 ∧ 𝑆 βŠ† 𝑁)))
222221rspcev 3580 . 2 ((𝑆 ∈ 𝐽 ∧ (𝑃 ∈ 𝑆 ∧ 𝑆 βŠ† 𝑁)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 ∧ 𝑒 βŠ† 𝑁))
223152, 174, 218, 222syl12anc 836 1 (πœ‘ β†’ βˆƒπ‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 ∧ 𝑒 βŠ† 𝑁))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406  Vcvv 3444   βˆ– cdif 3908   ∩ cin 3910   βŠ† wss 3911  βˆ…c0 4283  π’« cpw 4561  {csn 4587  βˆͺ cuni 4866  βˆͺ ciun 4955   ↦ cmpt 5189  ran crn 5635   β†Ύ cres 5636  suc csuc 6320   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  Ο‰com 7803  reccrdg 8356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357
This theorem is referenced by:  neibastop2  34879
  Copyright terms: Public domain W3C validator