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 33262
Description: Lemma for neibastop2 33263. (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 3941 . . . . 5 {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
31, 2eqsstri 3886 . . . 4 𝑆𝑋
4 neibastop1.1 . . . . 5 (𝜑𝑋𝑉)
5 elpw2g 5100 . . . . 5 (𝑋𝑉 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
64, 5syl 17 . . . 4 (𝜑 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
73, 6mpbiri 250 . . 3 (𝜑𝑆 ∈ 𝒫 𝑋)
8 fveq2 6497 . . . . . . . . 9 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
98ineq1d 4070 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑥) ∩ 𝒫 𝑓))
109neeq1d 3021 . . . . . . 7 (𝑦 = 𝑥 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1110rexbidv 3237 . . . . . 6 (𝑦 = 𝑥 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1211, 1elrab2 3594 . . . . 5 (𝑥𝑆 ↔ (𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13 frfnom 7873 . . . . . . . . . 10 (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14 neibastop2.g . . . . . . . . . . 11 𝐺 = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
1514fneq1i 6281 . . . . . . . . . 10 (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
1613, 15mpbir 223 . . . . . . . . 9 𝐺 Fn ω
17 fnunirn 6836 . . . . . . . . 9 (𝐺 Fn ω → (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
1816, 17ax-mp 5 . . . . . . . 8 (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
19 n0 4191 . . . . . . . . . 10 (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
20 inss1 4087 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹𝑥)
2120sseli 3849 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹𝑥))
22 neibastop1.6 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2322anassrs 460 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ (𝐹𝑥)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2421, 23sylan2 584 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2524adantrl 704 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26 simprl 759 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹𝑥))
27 fvssunirn 6526 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑥) ⊆ ran 𝐹
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
2928frnd 6349 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
3029difss2d 3996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
31 sspwuni 4885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ran 𝐹 ⊆ 𝒫 𝑋)
3230, 31sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 ran 𝐹 ⊆ 𝒫 𝑋)
3332ad2antrr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐹 ⊆ 𝒫 𝑋)
3427, 33syl5ss 3864 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐹𝑥) ⊆ 𝒫 𝑋)
3534sselda 3853 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡 ∈ 𝒫 𝑋)
3635elpwid 4429 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡𝑋)
3736sselda 3853 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → 𝑦𝑋)
3837adantrr 705 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑋)
39 simprlr 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺𝑘))
40 rspe 3244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝑋𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
4140ad2ant2l 734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
42 eliun 4793 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
43 pweq 4420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
4443ineq2d 4071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑓 → ((𝐹𝑥) ∩ 𝒫 𝑧) = ((𝐹𝑥) ∩ 𝒫 𝑓))
4544eleq2d 2846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4645rexbidv 3237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑓 → (∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4742, 46syl5bb 275 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑓 → (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4847rspcev 3530 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (𝐺𝑘) ∧ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
4939, 41, 48syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
50 eliun 4793 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
5149, 50sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
52 simpll 755 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝜑)
53 simprll 767 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
54 fvssunirn 6526 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺𝑘) ⊆ ran 𝐺
55 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑛 = ∅ → (𝐺𝑛) = (𝐺‘∅))
5614fveq1i 6498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
57 snex 5185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {𝑈} ∈ V
58 fr0g 7874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
5957, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
6056, 59eqtri 2797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝐺‘∅) = {𝑈}
6155, 60syl6eq 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = ∅ → (𝐺𝑛) = {𝑈})
6261sseq1d 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = ∅ → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
63 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
6463sseq1d 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺𝑘) ⊆ 𝒫 𝑈))
65 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = suc 𝑘 → (𝐺𝑛) = (𝐺‘suc 𝑘))
6665sseq1d 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = suc 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
67 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑈 ∈ (𝐹𝑃))
68 pwidg 4432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ 𝒫 𝑈)
6967, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝑈 ∈ 𝒫 𝑈)
7069snssd 4613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
71 simprl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
7267adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹𝑃))
7372pwexd 5130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
74 inss2 4088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
75 elpwi 4427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑧 ∈ 𝒫 𝑈𝑧𝑈)
7675adantl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑧𝑈)
77 sspwb 5195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑧𝑈 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑈)
7876, 77sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
7974, 78syl5ss 3864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑𝑧 ∈ 𝒫 𝑈) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8079ralrimivw 3128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑𝑧 ∈ 𝒫 𝑈) → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
81 iunss 4832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ( 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8280, 81sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8382ralrimiva 3127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
84 ssralv 3918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐺𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8584adantl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8683, 85mpan9 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
87 iunss 4832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ( 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8886, 87sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8973, 88ssexd 5081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V)
90 iuneq1 4804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑎 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
91 iuneq1 4804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = (𝐺𝑘) → 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9214, 90, 91frsucmpt2 7878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9371, 89, 92syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9493, 88eqsstrd 3890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
9594expr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ω) → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
9695expcom 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ω → (𝜑 → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
9762, 64, 66, 70, 96finds2 7424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ⊆ 𝒫 𝑈))
98 fvex 6510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐺𝑛) ∈ V
9998elpw 4423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺𝑛) ⊆ 𝒫 𝑈)
10097, 99syl6ibr 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
101100com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝑛 ∈ ω → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
102101ralrimiv 3126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
103 ffnfv 6704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
10416, 103mpbiran 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
105102, 104sylibr 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐺:ω⟶𝒫 𝒫 𝑈)
106105frnd 6349 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
107 sspwuni 4885 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ran 𝐺 ⊆ 𝒫 𝑈)
108106, 107sylib 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 ran 𝐺 ⊆ 𝒫 𝑈)
109108ad2antrr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐺 ⊆ 𝒫 𝑈)
11054, 109syl5ss 3864 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺𝑘) ⊆ 𝒫 𝑈)
11152, 53, 110, 93syl12anc 825 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
11251, 111eleqtrrd 2864 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
113 peano2 7416 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
11453, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
115 fnfvelrn 6672 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
11616, 114, 115sylancr 579 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
117 elunii 4714 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ran 𝐺)
118112, 116, 117syl2anc 576 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ran 𝐺)
119118ad2antrr 714 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ran 𝐺)
120 simprr 761 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
121 pweq 4420 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
122121ineq2d 4071 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑣 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑦) ∩ 𝒫 𝑣))
123122neeq1d 3021 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑣 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅))
124123rspcev 3530 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ran 𝐺 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
125119, 120, 124syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
1261rabeq2i 3405 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑆 ↔ (𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
12738, 125, 126sylanbrc 575 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑆)
128127expr 449 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → (((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦𝑆))
129128ralimdva 3122 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → (∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦𝑡 𝑦𝑆))
130129impr 447 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦𝑡 𝑦𝑆)
131 dfss3 3842 . . . . . . . . . . . . . . . 16 (𝑡𝑆 ↔ ∀𝑦𝑡 𝑦𝑆)
132130, 131sylibr 226 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡𝑆)
133 selpw 4424 . . . . . . . . . . . . . . 15 (𝑡 ∈ 𝒫 𝑆𝑡𝑆)
134132, 133sylibr 226 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
135 inelcm 4292 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝐹𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
13626, 134, 135syl2anc 576 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
13725, 136rexlimddv 3231 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
138137expr 449 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
139138exlimdv 1893 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14019, 139syl5bi 234 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
141140rexlimdvaa 3225 . . . . . . . 8 ((𝜑𝑥𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
14218, 141syl5bi 234 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
143142rexlimdv 3223 . . . . . 6 ((𝜑𝑥𝑋) → (∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144143expimpd 446 . . . . 5 (𝜑 → ((𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14512, 144syl5bi 234 . . . 4 (𝜑 → (𝑥𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
146145ralrimiv 3126 . . 3 (𝜑 → ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
147 pweq 4420 . . . . . . 7 (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
148147ineq2d 4071 . . . . . 6 (𝑜 = 𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑆))
149148neeq1d 3021 . . . . 5 (𝑜 = 𝑆 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
150149raleqbi1dv 3338 . . . 4 (𝑜 = 𝑆 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
151 neibastop1.4 . . . 4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
152150, 151elrab2 3594 . . 3 (𝑆𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
1537, 146, 152sylanbrc 575 . 2 (𝜑𝑆𝐽)
154 neibastop2.p . . 3 (𝜑𝑃𝑋)
155 snidg 4468 . . . . . 6 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ {𝑈})
15667, 155syl 17 . . . . 5 (𝜑𝑈 ∈ {𝑈})
157 peano1 7415 . . . . . . 7 ∅ ∈ ω
158 fnfvelrn 6672 . . . . . . 7 ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
15916, 157, 158mp2an 680 . . . . . 6 (𝐺‘∅) ∈ ran 𝐺
16060, 159eqeltrri 2858 . . . . 5 {𝑈} ∈ ran 𝐺
161 elunii 4714 . . . . 5 ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ran 𝐺)
162156, 160, 161sylancl 578 . . . 4 (𝜑𝑈 ran 𝐺)
163 inelcm 4292 . . . . 5 ((𝑈 ∈ (𝐹𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
16467, 69, 163syl2anc 576 . . . 4 (𝜑 → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
165 pweq 4420 . . . . . . 7 (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
166165ineq2d 4071 . . . . . 6 (𝑓 = 𝑈 → ((𝐹𝑃) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑈))
167166neeq1d 3021 . . . . 5 (𝑓 = 𝑈 → (((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅))
168167rspcev 3530 . . . 4 ((𝑈 ran 𝐺 ∧ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
169162, 164, 168syl2anc 576 . . 3 (𝜑 → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
170 fveq2 6497 . . . . . . 7 (𝑦 = 𝑃 → (𝐹𝑦) = (𝐹𝑃))
171170ineq1d 4070 . . . . . 6 (𝑦 = 𝑃 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑓))
172171neeq1d 3021 . . . . 5 (𝑦 = 𝑃 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
173172rexbidv 3237 . . . 4 (𝑦 = 𝑃 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
174173, 1elrab2 3594 . . 3 (𝑃𝑆 ↔ (𝑃𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
175154, 169, 174sylanbrc 575 . 2 (𝜑𝑃𝑆)
176 eluni2 4713 . . . . . . 7 (𝑓 ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓𝑧)
177 eleq2 2849 . . . . . . . . . 10 (𝑧 = (𝐺𝑘) → (𝑓𝑧𝑓 ∈ (𝐺𝑘)))
178177rexrn 6677 . . . . . . . . 9 (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
17916, 178ax-mp 5 . . . . . . . 8 (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
180105adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
181180ffvelrnda 6675 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ∈ 𝒫 𝒫 𝑈)
182181elpwid 4429 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ⊆ 𝒫 𝑈)
183182sselda 3853 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → 𝑓 ∈ 𝒫 𝑈)
184183adantrr 705 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
185184elpwid 4429 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑈)
186 neibastop2.u . . . . . . . . . . . . 13 (𝜑𝑈𝑁)
187186ad3antrrr 718 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈𝑁)
188185, 187sstrd 3863 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑁)
189 n0 4191 . . . . . . . . . . . . 13 (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓))
190 elin 4052 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
191 simprrr 770 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
192191elpwid 4429 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣𝑓)
193 simpllr 764 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑋)
194 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
195194expr 449 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝑋) → (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
196195ralrimiva 3127 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
197196ad3antrrr 718 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
198 simprrl 769 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹𝑦))
199 fveq2 6497 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
200199eleq2d 2846 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑣 ∈ (𝐹𝑥) ↔ 𝑣 ∈ (𝐹𝑦)))
201 elequ1 2058 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
202200, 201imbi12d 337 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) ↔ (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
203202rspcv 3526 . . . . . . . . . . . . . . . . . 18 (𝑦𝑋 → (∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) → (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
204193, 197, 198, 203syl3c 66 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑣)
205192, 204sseldd 3854 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑓)
206205expr 449 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → ((𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦𝑓))
207190, 206syl5bi 234 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
208207exlimdv 1893 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
209189, 208syl5bi 234 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑓))
210209impr 447 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑓)
211188, 210sseldd 3854 . . . . . . . . . 10 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑁)
212211exp32 413 . . . . . . . . 9 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
213212rexlimdva 3224 . . . . . . . 8 ((𝜑𝑦𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
214179, 213syl5bi 234 . . . . . . 7 ((𝜑𝑦𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
215176, 214syl5bi 234 . . . . . 6 ((𝜑𝑦𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
216215rexlimdv 3223 . . . . 5 ((𝜑𝑦𝑋) → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁))
2172163impia 1098 . . . 4 ((𝜑𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦𝑁)
218217rabssdv 3936 . . 3 (𝜑 → {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
2191, 218syl5eqss 3900 . 2 (𝜑𝑆𝑁)
220 eleq2 2849 . . . 4 (𝑢 = 𝑆 → (𝑃𝑢𝑃𝑆))
221 sseq1 3877 . . . 4 (𝑢 = 𝑆 → (𝑢𝑁𝑆𝑁))
222220, 221anbi12d 622 . . 3 (𝑢 = 𝑆 → ((𝑃𝑢𝑢𝑁) ↔ (𝑃𝑆𝑆𝑁)))
223222rspcev 3530 . 2 ((𝑆𝐽 ∧ (𝑃𝑆𝑆𝑁)) → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
224153, 175, 219, 223syl12anc 825 1 (𝜑 → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wex 1743  wcel 2051  wne 2962  wral 3083  wrex 3084  {crab 3087  Vcvv 3410  cdif 3821  cin 3823  wss 3824  c0 4173  𝒫 cpw 4417  {csn 4436   cuni 4709   ciun 4789  cmpt 5005  ran crn 5405  cres 5406  suc csuc 6029   Fn wfn 6181  wf 6182  cfv 6186  ωcom 7395  reccrdg 7848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-om 7396  df-wrecs 7749  df-recs 7811  df-rdg 7849
This theorem is referenced by:  neibastop2  33263
  Copyright terms: Public domain W3C validator