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 32692
Description: Lemma for neibastop2 32693. (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 3836 . . . . 5 {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
31, 2eqsstri 3784 . . . 4 𝑆𝑋
4 neibastop1.1 . . . . 5 (𝜑𝑋𝑉)
5 elpw2g 4958 . . . . 5 (𝑋𝑉 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
64, 5syl 17 . . . 4 (𝜑 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
73, 6mpbiri 248 . . 3 (𝜑𝑆 ∈ 𝒫 𝑋)
8 fveq2 6332 . . . . . . . . 9 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
98ineq1d 3964 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑥) ∩ 𝒫 𝑓))
109neeq1d 3002 . . . . . . 7 (𝑦 = 𝑥 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1110rexbidv 3200 . . . . . 6 (𝑦 = 𝑥 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1211, 1elrab2 3518 . . . . 5 (𝑥𝑆 ↔ (𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13 frfnom 7683 . . . . . . . . . 10 (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14 neibastop2.g . . . . . . . . . . 11 𝐺 = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
1514fneq1i 6125 . . . . . . . . . 10 (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
1613, 15mpbir 221 . . . . . . . . 9 𝐺 Fn ω
17 fnunirn 6654 . . . . . . . . 9 (𝐺 Fn ω → (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
1816, 17ax-mp 5 . . . . . . . 8 (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
19 n0 4078 . . . . . . . . . 10 (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
20 inss1 3981 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹𝑥)
2120sseli 3748 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹𝑥))
22 neibastop1.6 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2322anassrs 458 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ (𝐹𝑥)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2421, 23sylan2 580 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2524adantrl 695 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26 simprl 754 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹𝑥))
27 fvssunirn 6358 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑥) ⊆ ran 𝐹
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
29 frn 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
3028, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
3130difss2d 3891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
32 sspwuni 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ran 𝐹 ⊆ 𝒫 𝑋)
3331, 32sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 ran 𝐹 ⊆ 𝒫 𝑋)
3433ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐹 ⊆ 𝒫 𝑋)
3527, 34syl5ss 3763 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐹𝑥) ⊆ 𝒫 𝑋)
3635sselda 3752 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡 ∈ 𝒫 𝑋)
3736elpwid 4309 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡𝑋)
3837sselda 3752 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → 𝑦𝑋)
3938adantrr 696 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑋)
40 simprlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺𝑘))
41 rspe 3151 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝑋𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
4241ad2ant2l 740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
43 eliun 4658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
44 pweq 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
4544ineq2d 3965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑓 → ((𝐹𝑥) ∩ 𝒫 𝑧) = ((𝐹𝑥) ∩ 𝒫 𝑓))
4645eleq2d 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4746rexbidv 3200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑓 → (∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4843, 47syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑓 → (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4948rspcev 3460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (𝐺𝑘) ∧ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
5040, 42, 49syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
51 eliun 4658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
5250, 51sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
53 simpll 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝜑)
54 simprll 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
55 fvssunirn 6358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺𝑘) ⊆ ran 𝐺
56 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑛 = ∅ → (𝐺𝑛) = (𝐺‘∅))
5714fveq1i 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
58 snex 5036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {𝑈} ∈ V
59 fr0g 7684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
6157, 60eqtri 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝐺‘∅) = {𝑈}
6256, 61syl6eq 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = ∅ → (𝐺𝑛) = {𝑈})
6362sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = ∅ → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
64 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
6564sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺𝑘) ⊆ 𝒫 𝑈))
66 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = suc 𝑘 → (𝐺𝑛) = (𝐺‘suc 𝑘))
6766sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = suc 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
68 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑈 ∈ (𝐹𝑃))
69 pwidg 4312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ 𝒫 𝑈)
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝑈 ∈ 𝒫 𝑈)
7170snssd 4475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
72 simprl 754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
7368adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹𝑃))
74 pwexg 4980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑈 ∈ (𝐹𝑃) → 𝒫 𝑈 ∈ V)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
76 inss2 3982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
77 elpwi 4307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑧 ∈ 𝒫 𝑈𝑧𝑈)
7877adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑧𝑈)
79 sspwb 5045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑧𝑈 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑈)
8078, 79sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
8176, 80syl5ss 3763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑𝑧 ∈ 𝒫 𝑈) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8281ralrimivw 3116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑𝑧 ∈ 𝒫 𝑈) → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
83 iunss 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ( 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8482, 83sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8584ralrimiva 3115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
86 ssralv 3815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐺𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8786adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8885, 87mpan9 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
89 iunss 4695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ( 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
9088, 89sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
9175, 90ssexd 4939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V)
92 iuneq1 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑎 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
93 iuneq1 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = (𝐺𝑘) → 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9414, 92, 93frsucmpt2 7688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9572, 91, 94syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9695, 90eqsstrd 3788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
9796expr 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ω) → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
9897expcom 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ω → (𝜑 → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
9963, 65, 67, 71, 98finds2 7241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ⊆ 𝒫 𝑈))
100 fvex 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐺𝑛) ∈ V
101100elpw 4303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺𝑛) ⊆ 𝒫 𝑈)
10299, 101syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
103102com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝑛 ∈ ω → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
104103ralrimiv 3114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
105 ffnfv 6530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
10616, 105mpbiran 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
107104, 106sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐺:ω⟶𝒫 𝒫 𝑈)
108 frn 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐺:ω⟶𝒫 𝒫 𝑈 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
110 sspwuni 4745 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ran 𝐺 ⊆ 𝒫 𝑈)
111109, 110sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 ran 𝐺 ⊆ 𝒫 𝑈)
112111ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐺 ⊆ 𝒫 𝑈)
11355, 112syl5ss 3763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺𝑘) ⊆ 𝒫 𝑈)
11453, 54, 113, 95syl12anc 1474 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
11552, 114eleqtrrd 2853 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
116 peano2 7233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
11754, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
118 fnfvelrn 6499 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
11916, 117, 118sylancr 575 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
120 elunii 4579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ran 𝐺)
121115, 119, 120syl2anc 573 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ran 𝐺)
122121ad2antrr 705 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ran 𝐺)
123 simprr 756 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
124 pweq 4300 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
125124ineq2d 3965 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑣 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑦) ∩ 𝒫 𝑣))
126125neeq1d 3002 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑣 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅))
127126rspcev 3460 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ran 𝐺 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
128122, 123, 127syl2anc 573 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
1291rabeq2i 3347 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑆 ↔ (𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
13039, 128, 129sylanbrc 572 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑆)
131130expr 444 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → (((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦𝑆))
132131ralimdva 3111 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → (∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦𝑡 𝑦𝑆))
133132impr 442 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦𝑡 𝑦𝑆)
134 dfss3 3741 . . . . . . . . . . . . . . . 16 (𝑡𝑆 ↔ ∀𝑦𝑡 𝑦𝑆)
135133, 134sylibr 224 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡𝑆)
136 selpw 4304 . . . . . . . . . . . . . . 15 (𝑡 ∈ 𝒫 𝑆𝑡𝑆)
137135, 136sylibr 224 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
138 inelcm 4175 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝐹𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
13926, 137, 138syl2anc 573 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
14025, 139rexlimddv 3183 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
141140expr 444 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
142141exlimdv 2013 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14319, 142syl5bi 232 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144143rexlimdvaa 3180 . . . . . . . 8 ((𝜑𝑥𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
14518, 144syl5bi 232 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
146145rexlimdv 3178 . . . . . 6 ((𝜑𝑥𝑋) → (∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
147146expimpd 441 . . . . 5 (𝜑 → ((𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14812, 147syl5bi 232 . . . 4 (𝜑 → (𝑥𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
149148ralrimiv 3114 . . 3 (𝜑 → ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
150 pweq 4300 . . . . . . 7 (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
151150ineq2d 3965 . . . . . 6 (𝑜 = 𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑆))
152151neeq1d 3002 . . . . 5 (𝑜 = 𝑆 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
153152raleqbi1dv 3295 . . . 4 (𝑜 = 𝑆 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
154 neibastop1.4 . . . 4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
155153, 154elrab2 3518 . . 3 (𝑆𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
1567, 149, 155sylanbrc 572 . 2 (𝜑𝑆𝐽)
157 neibastop2.p . . 3 (𝜑𝑃𝑋)
158 snidg 4345 . . . . . 6 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ {𝑈})
15968, 158syl 17 . . . . 5 (𝜑𝑈 ∈ {𝑈})
160 peano1 7232 . . . . . . 7 ∅ ∈ ω
161 fnfvelrn 6499 . . . . . . 7 ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
16216, 160, 161mp2an 672 . . . . . 6 (𝐺‘∅) ∈ ran 𝐺
16361, 162eqeltrri 2847 . . . . 5 {𝑈} ∈ ran 𝐺
164 elunii 4579 . . . . 5 ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ran 𝐺)
165159, 163, 164sylancl 574 . . . 4 (𝜑𝑈 ran 𝐺)
166 inelcm 4175 . . . . 5 ((𝑈 ∈ (𝐹𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
16768, 70, 166syl2anc 573 . . . 4 (𝜑 → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
168 pweq 4300 . . . . . . 7 (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
169168ineq2d 3965 . . . . . 6 (𝑓 = 𝑈 → ((𝐹𝑃) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑈))
170169neeq1d 3002 . . . . 5 (𝑓 = 𝑈 → (((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅))
171170rspcev 3460 . . . 4 ((𝑈 ran 𝐺 ∧ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
172165, 167, 171syl2anc 573 . . 3 (𝜑 → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
173 fveq2 6332 . . . . . . 7 (𝑦 = 𝑃 → (𝐹𝑦) = (𝐹𝑃))
174173ineq1d 3964 . . . . . 6 (𝑦 = 𝑃 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑓))
175174neeq1d 3002 . . . . 5 (𝑦 = 𝑃 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
176175rexbidv 3200 . . . 4 (𝑦 = 𝑃 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
177176, 1elrab2 3518 . . 3 (𝑃𝑆 ↔ (𝑃𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
178157, 172, 177sylanbrc 572 . 2 (𝜑𝑃𝑆)
179 eluni2 4578 . . . . . . 7 (𝑓 ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓𝑧)
180 eleq2 2839 . . . . . . . . . 10 (𝑧 = (𝐺𝑘) → (𝑓𝑧𝑓 ∈ (𝐺𝑘)))
181180rexrn 6504 . . . . . . . . 9 (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
18216, 181ax-mp 5 . . . . . . . 8 (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
183107adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
184183ffvelrnda 6502 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ∈ 𝒫 𝒫 𝑈)
185184elpwid 4309 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ⊆ 𝒫 𝑈)
186185sselda 3752 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → 𝑓 ∈ 𝒫 𝑈)
187186adantrr 696 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
188187elpwid 4309 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑈)
189 neibastop2.u . . . . . . . . . . . . 13 (𝜑𝑈𝑁)
190189ad3antrrr 709 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈𝑁)
191188, 190sstrd 3762 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑁)
192 n0 4078 . . . . . . . . . . . . 13 (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓))
193 elin 3947 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
194 simprrr 767 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
195194elpwid 4309 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣𝑓)
196 simpllr 760 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑋)
197 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
198197expr 444 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝑋) → (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
199198ralrimiva 3115 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
200199ad3antrrr 709 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
201 simprrl 766 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹𝑦))
202 fveq2 6332 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
203202eleq2d 2836 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑣 ∈ (𝐹𝑥) ↔ 𝑣 ∈ (𝐹𝑦)))
204 elequ1 2152 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
205203, 204imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) ↔ (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
206205rspcv 3456 . . . . . . . . . . . . . . . . . 18 (𝑦𝑋 → (∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) → (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
207196, 200, 201, 206syl3c 66 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑣)
208195, 207sseldd 3753 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑓)
209208expr 444 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → ((𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦𝑓))
210193, 209syl5bi 232 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
211210exlimdv 2013 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
212192, 211syl5bi 232 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑓))
213212impr 442 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑓)
214191, 213sseldd 3753 . . . . . . . . . 10 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑁)
215214exp32 407 . . . . . . . . 9 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
216215rexlimdva 3179 . . . . . . . 8 ((𝜑𝑦𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
217182, 216syl5bi 232 . . . . . . 7 ((𝜑𝑦𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
218179, 217syl5bi 232 . . . . . 6 ((𝜑𝑦𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
219218rexlimdv 3178 . . . . 5 ((𝜑𝑦𝑋) → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁))
2202193impia 1109 . . . 4 ((𝜑𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦𝑁)
221220rabssdv 3831 . . 3 (𝜑 → {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
2221, 221syl5eqss 3798 . 2 (𝜑𝑆𝑁)
223 eleq2 2839 . . . 4 (𝑢 = 𝑆 → (𝑃𝑢𝑃𝑆))
224 sseq1 3775 . . . 4 (𝑢 = 𝑆 → (𝑢𝑁𝑆𝑁))
225223, 224anbi12d 616 . . 3 (𝑢 = 𝑆 → ((𝑃𝑢𝑢𝑁) ↔ (𝑃𝑆𝑆𝑁)))
226225rspcev 3460 . 2 ((𝑆𝐽 ∧ (𝑃𝑆𝑆𝑁)) → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
227156, 178, 222, 226syl12anc 1474 1 (𝜑 → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cdif 3720  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  {csn 4316   cuni 4574   ciun 4654  cmpt 4863  ran crn 5250  cres 5251  suc csuc 5868   Fn wfn 6026  wf 6027  cfv 6031  ωcom 7212  reccrdg 7658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659
This theorem is referenced by:  neibastop2  32693
  Copyright terms: Public domain W3C validator