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 32330
Description: Lemma for neibastop2 32331. (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 3679 . . . . 5 {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
31, 2eqsstri 3627 . . . 4 𝑆𝑋
4 neibastop1.1 . . . . 5 (𝜑𝑋𝑉)
5 elpw2g 4818 . . . . 5 (𝑋𝑉 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
64, 5syl 17 . . . 4 (𝜑 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
73, 6mpbiri 248 . . 3 (𝜑𝑆 ∈ 𝒫 𝑋)
8 fveq2 6178 . . . . . . . . 9 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
98ineq1d 3805 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑥) ∩ 𝒫 𝑓))
109neeq1d 2850 . . . . . . 7 (𝑦 = 𝑥 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1110rexbidv 3048 . . . . . 6 (𝑦 = 𝑥 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1211, 1elrab2 3360 . . . . 5 (𝑥𝑆 ↔ (𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13 frfnom 7515 . . . . . . . . . 10 (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14 neibastop2.g . . . . . . . . . . 11 𝐺 = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
1514fneq1i 5973 . . . . . . . . . 10 (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
1613, 15mpbir 221 . . . . . . . . 9 𝐺 Fn ω
17 fnunirn 6496 . . . . . . . . 9 (𝐺 Fn ω → (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
1816, 17ax-mp 5 . . . . . . . 8 (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
19 n0 3923 . . . . . . . . . 10 (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
20 inss1 3825 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹𝑥)
2120sseli 3591 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹𝑥))
22 neibastop1.6 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2322anassrs 679 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ (𝐹𝑥)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2421, 23sylan2 491 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2524adantrl 751 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26 simprl 793 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹𝑥))
27 fvssunirn 6204 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑥) ⊆ ran 𝐹
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
29 frn 6040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
3028, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
3130difss2d 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
32 sspwuni 4602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ran 𝐹 ⊆ 𝒫 𝑋)
3331, 32sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 ran 𝐹 ⊆ 𝒫 𝑋)
3433ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐹 ⊆ 𝒫 𝑋)
3527, 34syl5ss 3606 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐹𝑥) ⊆ 𝒫 𝑋)
3635sselda 3595 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡 ∈ 𝒫 𝑋)
3736elpwid 4161 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡𝑋)
3837sselda 3595 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → 𝑦𝑋)
3938adantrr 752 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑋)
40 simprlr 802 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺𝑘))
41 rspe 3000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝑋𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
4241ad2ant2l 781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
43 eliun 4515 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
44 pweq 4152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
4544ineq2d 3806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑓 → ((𝐹𝑥) ∩ 𝒫 𝑧) = ((𝐹𝑥) ∩ 𝒫 𝑓))
4645eleq2d 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4746rexbidv 3048 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑓 → (∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4843, 47syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑓 → (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4948rspcev 3304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (𝐺𝑘) ∧ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
5040, 42, 49syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
51 eliun 4515 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
5250, 51sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
53 simpll 789 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝜑)
54 simprll 801 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
55 fvssunirn 6204 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺𝑘) ⊆ ran 𝐺
56 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑛 = ∅ → (𝐺𝑛) = (𝐺‘∅))
5714fveq1i 6179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
58 snex 4899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {𝑈} ∈ V
59 fr0g 7516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
6157, 60eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝐺‘∅) = {𝑈}
6256, 61syl6eq 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = ∅ → (𝐺𝑛) = {𝑈})
6362sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = ∅ → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
64 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
6564sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺𝑘) ⊆ 𝒫 𝑈))
66 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = suc 𝑘 → (𝐺𝑛) = (𝐺‘suc 𝑘))
6766sseq1d 3624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = suc 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
68 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑈 ∈ (𝐹𝑃))
69 pwidg 4164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ 𝒫 𝑈)
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝑈 ∈ 𝒫 𝑈)
7170snssd 4331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
72 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
7368adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹𝑃))
74 pwexg 4841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑈 ∈ (𝐹𝑃) → 𝒫 𝑈 ∈ V)
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
76 inss2 3826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
77 elpwi 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑧 ∈ 𝒫 𝑈𝑧𝑈)
7877adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑧𝑈)
79 sspwb 4908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑧𝑈 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑈)
8078, 79sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
8176, 80syl5ss 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑𝑧 ∈ 𝒫 𝑈) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8281ralrimivw 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑𝑧 ∈ 𝒫 𝑈) → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
83 iunss 4552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ( 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8482, 83sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8584ralrimiva 2963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
86 ssralv 3658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐺𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8786adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8885, 87mpan9 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
89 iunss 4552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ( 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
9088, 89sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
9175, 90ssexd 4796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V)
92 iuneq1 4525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑎 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
93 iuneq1 4525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = (𝐺𝑘) → 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9414, 92, 93frsucmpt2 7520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9572, 91, 94syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9695, 90eqsstrd 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
9796expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ω) → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
9897expcom 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ω → (𝜑 → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
9963, 65, 67, 71, 98finds2 7079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ⊆ 𝒫 𝑈))
100 fvex 6188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐺𝑛) ∈ V
101100elpw 4155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺𝑛) ⊆ 𝒫 𝑈)
10299, 101syl6ibr 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
103102com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝑛 ∈ ω → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
104103ralrimiv 2962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
105 ffnfv 6374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
10616, 105mpbiran 952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
107104, 106sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐺:ω⟶𝒫 𝒫 𝑈)
108 frn 6040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐺:ω⟶𝒫 𝒫 𝑈 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
110 sspwuni 4602 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ran 𝐺 ⊆ 𝒫 𝑈)
111109, 110sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 ran 𝐺 ⊆ 𝒫 𝑈)
112111ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐺 ⊆ 𝒫 𝑈)
11355, 112syl5ss 3606 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺𝑘) ⊆ 𝒫 𝑈)
11453, 54, 113, 95syl12anc 1322 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
11552, 114eleqtrrd 2702 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
116 peano2 7071 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
11754, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
118 fnfvelrn 6342 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
11916, 117, 118sylancr 694 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
120 elunii 4432 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ran 𝐺)
121115, 119, 120syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ran 𝐺)
122121ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ran 𝐺)
123 simprr 795 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
124 pweq 4152 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
125124ineq2d 3806 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑣 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑦) ∩ 𝒫 𝑣))
126125neeq1d 2850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑣 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅))
127126rspcev 3304 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ran 𝐺 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
128122, 123, 127syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
1291rabeq2i 3192 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑆 ↔ (𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
13039, 128, 129sylanbrc 697 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑆)
131130expr 642 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → (((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦𝑆))
132131ralimdva 2959 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → (∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦𝑡 𝑦𝑆))
133132impr 648 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦𝑡 𝑦𝑆)
134 dfss3 3585 . . . . . . . . . . . . . . . 16 (𝑡𝑆 ↔ ∀𝑦𝑡 𝑦𝑆)
135133, 134sylibr 224 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡𝑆)
136 selpw 4156 . . . . . . . . . . . . . . 15 (𝑡 ∈ 𝒫 𝑆𝑡𝑆)
137135, 136sylibr 224 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
138 inelcm 4023 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝐹𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
13926, 137, 138syl2anc 692 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
14025, 139rexlimddv 3031 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
141140expr 642 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
142141exlimdv 1859 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14319, 142syl5bi 232 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144143rexlimdvaa 3028 . . . . . . . 8 ((𝜑𝑥𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
14518, 144syl5bi 232 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
146145rexlimdv 3026 . . . . . 6 ((𝜑𝑥𝑋) → (∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
147146expimpd 628 . . . . 5 (𝜑 → ((𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14812, 147syl5bi 232 . . . 4 (𝜑 → (𝑥𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
149148ralrimiv 2962 . . 3 (𝜑 → ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
150 pweq 4152 . . . . . . 7 (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
151150ineq2d 3806 . . . . . 6 (𝑜 = 𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑆))
152151neeq1d 2850 . . . . 5 (𝑜 = 𝑆 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
153152raleqbi1dv 3141 . . . 4 (𝑜 = 𝑆 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
154 neibastop1.4 . . . 4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
155153, 154elrab2 3360 . . 3 (𝑆𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
1567, 149, 155sylanbrc 697 . 2 (𝜑𝑆𝐽)
157 neibastop2.p . . 3 (𝜑𝑃𝑋)
158 snidg 4197 . . . . . 6 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ {𝑈})
15968, 158syl 17 . . . . 5 (𝜑𝑈 ∈ {𝑈})
160 peano1 7070 . . . . . . 7 ∅ ∈ ω
161 fnfvelrn 6342 . . . . . . 7 ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
16216, 160, 161mp2an 707 . . . . . 6 (𝐺‘∅) ∈ ran 𝐺
16361, 162eqeltrri 2696 . . . . 5 {𝑈} ∈ ran 𝐺
164 elunii 4432 . . . . 5 ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ran 𝐺)
165159, 163, 164sylancl 693 . . . 4 (𝜑𝑈 ran 𝐺)
166 inelcm 4023 . . . . 5 ((𝑈 ∈ (𝐹𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
16768, 70, 166syl2anc 692 . . . 4 (𝜑 → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
168 pweq 4152 . . . . . . 7 (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
169168ineq2d 3806 . . . . . 6 (𝑓 = 𝑈 → ((𝐹𝑃) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑈))
170169neeq1d 2850 . . . . 5 (𝑓 = 𝑈 → (((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅))
171170rspcev 3304 . . . 4 ((𝑈 ran 𝐺 ∧ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
172165, 167, 171syl2anc 692 . . 3 (𝜑 → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
173 fveq2 6178 . . . . . . 7 (𝑦 = 𝑃 → (𝐹𝑦) = (𝐹𝑃))
174173ineq1d 3805 . . . . . 6 (𝑦 = 𝑃 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑓))
175174neeq1d 2850 . . . . 5 (𝑦 = 𝑃 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
176175rexbidv 3048 . . . 4 (𝑦 = 𝑃 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
177176, 1elrab2 3360 . . 3 (𝑃𝑆 ↔ (𝑃𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
178157, 172, 177sylanbrc 697 . 2 (𝜑𝑃𝑆)
179 eluni2 4431 . . . . . . 7 (𝑓 ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓𝑧)
180 eleq2 2688 . . . . . . . . . 10 (𝑧 = (𝐺𝑘) → (𝑓𝑧𝑓 ∈ (𝐺𝑘)))
181180rexrn 6347 . . . . . . . . 9 (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
18216, 181ax-mp 5 . . . . . . . 8 (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
183107adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
184183ffvelrnda 6345 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ∈ 𝒫 𝒫 𝑈)
185184elpwid 4161 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ⊆ 𝒫 𝑈)
186185sselda 3595 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → 𝑓 ∈ 𝒫 𝑈)
187186adantrr 752 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
188187elpwid 4161 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑈)
189 neibastop2.u . . . . . . . . . . . . 13 (𝜑𝑈𝑁)
190189ad3antrrr 765 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈𝑁)
191188, 190sstrd 3605 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑁)
192 n0 3923 . . . . . . . . . . . . 13 (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓))
193 elin 3788 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
194 simprrr 804 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
195194elpwid 4161 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣𝑓)
196 simpllr 798 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑋)
197 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
198197expr 642 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝑋) → (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
199198ralrimiva 2963 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
200199ad3antrrr 765 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
201 simprrl 803 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹𝑦))
202 fveq2 6178 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
203202eleq2d 2685 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑣 ∈ (𝐹𝑥) ↔ 𝑣 ∈ (𝐹𝑦)))
204 elequ1 1995 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
205203, 204imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) ↔ (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
206205rspcv 3300 . . . . . . . . . . . . . . . . . 18 (𝑦𝑋 → (∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) → (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
207196, 200, 201, 206syl3c 66 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑣)
208195, 207sseldd 3596 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑓)
209208expr 642 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → ((𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦𝑓))
210193, 209syl5bi 232 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
211210exlimdv 1859 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
212192, 211syl5bi 232 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑓))
213212impr 648 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑓)
214191, 213sseldd 3596 . . . . . . . . . 10 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑁)
215214exp32 630 . . . . . . . . 9 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
216215rexlimdva 3027 . . . . . . . 8 ((𝜑𝑦𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
217182, 216syl5bi 232 . . . . . . 7 ((𝜑𝑦𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
218179, 217syl5bi 232 . . . . . 6 ((𝜑𝑦𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
219218rexlimdv 3026 . . . . 5 ((𝜑𝑦𝑋) → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁))
2202193impia 1259 . . . 4 ((𝜑𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦𝑁)
221220rabssdv 3674 . . 3 (𝜑 → {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
2221, 221syl5eqss 3641 . 2 (𝜑𝑆𝑁)
223 eleq2 2688 . . . 4 (𝑢 = 𝑆 → (𝑃𝑢𝑃𝑆))
224 sseq1 3618 . . . 4 (𝑢 = 𝑆 → (𝑢𝑁𝑆𝑁))
225223, 224anbi12d 746 . . 3 (𝑢 = 𝑆 → ((𝑃𝑢𝑢𝑁) ↔ (𝑃𝑆𝑆𝑁)))
226225rspcev 3304 . 2 ((𝑆𝐽 ∧ (𝑃𝑆𝑆𝑁)) → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
227156, 178, 222, 226syl12anc 1322 1 (𝜑 → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wex 1702  wcel 1988  wne 2791  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149  {csn 4168   cuni 4427   ciun 4511  cmpt 4720  ran crn 5105  cres 5106  suc csuc 5713   Fn wfn 5871  wf 5872  cfv 5876  ωcom 7050  reccrdg 7490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491
This theorem is referenced by:  neibastop2  32331
  Copyright terms: Public domain W3C validator