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 32819
Description: Lemma for neibastop2 32820. (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 3849 . . . . 5 {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑋
31, 2eqsstri 3797 . . . 4 𝑆𝑋
4 neibastop1.1 . . . . 5 (𝜑𝑋𝑉)
5 elpw2g 4987 . . . . 5 (𝑋𝑉 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
64, 5syl 17 . . . 4 (𝜑 → (𝑆 ∈ 𝒫 𝑋𝑆𝑋))
73, 6mpbiri 249 . . 3 (𝜑𝑆 ∈ 𝒫 𝑋)
8 fveq2 6379 . . . . . . . . 9 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
98ineq1d 3977 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑥) ∩ 𝒫 𝑓))
109neeq1d 2996 . . . . . . 7 (𝑦 = 𝑥 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1110rexbidv 3199 . . . . . 6 (𝑦 = 𝑥 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
1211, 1elrab2 3525 . . . . 5 (𝑥𝑆 ↔ (𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅))
13 frfnom 7738 . . . . . . . . . 10 (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω
14 neibastop2.g . . . . . . . . . . 11 𝐺 = (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)
1514fneq1i 6165 . . . . . . . . . 10 (𝐺 Fn ω ↔ (rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω) Fn ω)
1613, 15mpbir 222 . . . . . . . . 9 𝐺 Fn ω
17 fnunirn 6707 . . . . . . . . 9 (𝐺 Fn ω → (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
1816, 17ax-mp 5 . . . . . . . 8 (𝑓 ran 𝐺 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
19 n0 4097 . . . . . . . . . 10 (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
20 inss1 3994 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑓) ⊆ (𝐹𝑥)
2120sseli 3759 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → 𝑣 ∈ (𝐹𝑥))
22 neibastop1.6 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2322anassrs 459 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ (𝐹𝑥)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2421, 23sylan2 586 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
2524adantrl 707 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑡 ∈ (𝐹𝑥)∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
26 simprl 787 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ (𝐹𝑥))
27 fvssunirn 6408 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑥) ⊆ ran 𝐹
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
2928frnd 6232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐹 ⊆ (𝒫 𝒫 𝑋 ∖ {∅}))
3029difss2d 3904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran 𝐹 ⊆ 𝒫 𝒫 𝑋)
31 sspwuni 4770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ran 𝐹 ⊆ 𝒫 𝒫 𝑋 ran 𝐹 ⊆ 𝒫 𝑋)
3230, 31sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 ran 𝐹 ⊆ 𝒫 𝑋)
3332ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐹 ⊆ 𝒫 𝑋)
3427, 33syl5ss 3774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐹𝑥) ⊆ 𝒫 𝑋)
3534sselda 3763 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡 ∈ 𝒫 𝑋)
3635elpwid 4329 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → 𝑡𝑋)
3736sselda 3763 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → 𝑦𝑋)
3837adantrr 708 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑋)
39 simprlr 798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑓 ∈ (𝐺𝑘))
40 rspe 3149 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝑋𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
4140ad2ant2l 752 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))
42 eliun 4682 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
43 pweq 4320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑧 = 𝑓 → 𝒫 𝑧 = 𝒫 𝑓)
4443ineq2d 3978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑧 = 𝑓 → ((𝐹𝑥) ∩ 𝒫 𝑧) = ((𝐹𝑥) ∩ 𝒫 𝑓))
4544eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑓 → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4645rexbidv 3199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑓 → (∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4742, 46syl5bb 274 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑓 → (𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)))
4847rspcev 3462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ (𝐺𝑘) ∧ ∃𝑥𝑋 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓)) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
4939, 41, 48syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
50 eliun 4682 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ↔ ∃𝑧 ∈ (𝐺𝑘)𝑣 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
5149, 50sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
52 simpll 783 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝜑)
53 simprll 797 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑘 ∈ ω)
54 fvssunirn 6408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐺𝑘) ⊆ ran 𝐺
55 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑛 = ∅ → (𝐺𝑛) = (𝐺‘∅))
5614fveq1i 6380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐺‘∅) = ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅)
57 snex 5066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 {𝑈} ∈ V
58 fr0g 7739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ({𝑈} ∈ V → ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈})
5957, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((rec((𝑎 ∈ V ↦ 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧)), {𝑈}) ↾ ω)‘∅) = {𝑈}
6056, 59eqtri 2787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝐺‘∅) = {𝑈}
6155, 60syl6eq 2815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = ∅ → (𝐺𝑛) = {𝑈})
6261sseq1d 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = ∅ → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ {𝑈} ⊆ 𝒫 𝑈))
63 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
6463sseq1d 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺𝑘) ⊆ 𝒫 𝑈))
65 fveq2 6379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑛 = suc 𝑘 → (𝐺𝑛) = (𝐺‘suc 𝑘))
6665sseq1d 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑛 = suc 𝑘 → ((𝐺𝑛) ⊆ 𝒫 𝑈 ↔ (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
67 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑𝑈 ∈ (𝐹𝑃))
68 pwidg 4332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ 𝒫 𝑈)
6967, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑𝑈 ∈ 𝒫 𝑈)
7069snssd 4496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → {𝑈} ⊆ 𝒫 𝑈)
71 simprl 787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑘 ∈ ω)
7267adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑈 ∈ (𝐹𝑃))
7372pwexd 5017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝒫 𝑈 ∈ V)
74 inss2 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
75 elpwi 4327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑧 ∈ 𝒫 𝑈𝑧𝑈)
7675adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑧𝑈)
77 sspwb 5075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑧𝑈 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑈)
7876, 77sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝒫 𝑧 ⊆ 𝒫 𝑈)
7974, 78syl5ss 3774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝜑𝑧 ∈ 𝒫 𝑈) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8079ralrimivw 3114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝜑𝑧 ∈ 𝒫 𝑈) → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
81 iunss 4719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ( 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8280, 81sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝜑𝑧 ∈ 𝒫 𝑈) → 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8382ralrimiva 3113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
84 ssralv 3828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝐺𝑘) ⊆ 𝒫 𝑈 → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8584adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈) → (∀𝑧 ∈ 𝒫 𝑈 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈))
8683, 85mpan9 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
87 iunss 4719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ( 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈 ↔ ∀𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8886, 87sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑈)
8973, 88ssexd 4968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V)
90 iuneq1 4692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = 𝑎 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧𝑎 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
91 iuneq1 4692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 = (𝐺𝑘) → 𝑧𝑦 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9214, 90, 91frsucmpt2 7743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧) ∈ V) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9371, 89, 92syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
9493, 88eqsstrd 3801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑 ∧ (𝑘 ∈ ω ∧ (𝐺𝑘) ⊆ 𝒫 𝑈)) → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)
9594expr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑘 ∈ ω) → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈))
9695expcom 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑘 ∈ ω → (𝜑 → ((𝐺𝑘) ⊆ 𝒫 𝑈 → (𝐺‘suc 𝑘) ⊆ 𝒫 𝑈)))
9762, 64, 66, 70, 96finds2 7296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ⊆ 𝒫 𝑈))
98 fvex 6392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐺𝑛) ∈ V
9998elpw 4323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑛) ∈ 𝒫 𝒫 𝑈 ↔ (𝐺𝑛) ⊆ 𝒫 𝑈)
10097, 99syl6ibr 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 ∈ ω → (𝜑 → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
101100com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝑛 ∈ ω → (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
102101ralrimiv 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
103 ffnfv 6582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈))
10416, 103mpbiran 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐺:ω⟶𝒫 𝒫 𝑈 ↔ ∀𝑛 ∈ ω (𝐺𝑛) ∈ 𝒫 𝒫 𝑈)
105102, 104sylibr 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐺:ω⟶𝒫 𝒫 𝑈)
106105frnd 6232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ran 𝐺 ⊆ 𝒫 𝒫 𝑈)
107 sspwuni 4770 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran 𝐺 ⊆ 𝒫 𝒫 𝑈 ran 𝐺 ⊆ 𝒫 𝑈)
108106, 107sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 ran 𝐺 ⊆ 𝒫 𝑈)
109108ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ran 𝐺 ⊆ 𝒫 𝑈)
11054, 109syl5ss 3774 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺𝑘) ⊆ 𝒫 𝑈)
11152, 53, 110, 93syl12anc 865 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) = 𝑧 ∈ (𝐺𝑘) 𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑧))
11251, 111eleqtrrd 2847 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ∈ (𝐺‘suc 𝑘))
113 peano2 7288 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
11453, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → suc 𝑘 ∈ ω)
115 fnfvelrn 6550 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn ω ∧ suc 𝑘 ∈ ω) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
11616, 114, 115sylancr 581 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → (𝐺‘suc 𝑘) ∈ ran 𝐺)
117 elunii 4601 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑣 ∈ (𝐺‘suc 𝑘) ∧ (𝐺‘suc 𝑘) ∈ ran 𝐺) → 𝑣 ran 𝐺)
118112, 116, 117syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → 𝑣 ran 𝐺)
119118ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑣 ran 𝐺)
120 simprr 789 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)
121 pweq 4320 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑣 → 𝒫 𝑓 = 𝒫 𝑣)
122121ineq2d 3978 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑣 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑦) ∩ 𝒫 𝑣))
123122neeq1d 2996 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑣 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅))
124123rspcev 3462 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 ran 𝐺 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
125119, 120, 124syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)
1261rabeq2i 3346 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑆 ↔ (𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅))
12738, 125, 126sylanbrc 578 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ (𝑦𝑡 ∧ ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑦𝑆)
128127expr 448 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) ∧ 𝑦𝑡) → (((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → 𝑦𝑆))
129128ralimdva 3109 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ 𝑡 ∈ (𝐹𝑥)) → (∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅ → ∀𝑦𝑡 𝑦𝑆))
130129impr 446 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ∀𝑦𝑡 𝑦𝑆)
131 dfss3 3752 . . . . . . . . . . . . . . . 16 (𝑡𝑆 ↔ ∀𝑦𝑡 𝑦𝑆)
132130, 131sylibr 225 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡𝑆)
133 selpw 4324 . . . . . . . . . . . . . . 15 (𝑡 ∈ 𝒫 𝑆𝑡𝑆)
134132, 133sylibr 225 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → 𝑡 ∈ 𝒫 𝑆)
135 inelcm 4195 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝐹𝑥) ∧ 𝑡 ∈ 𝒫 𝑆) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
13626, 134, 135syl2anc 579 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) ∧ (𝑡 ∈ (𝐹𝑥) ∧ ∀𝑦𝑡 ((𝐹𝑦) ∩ 𝒫 𝑣) ≠ ∅)) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
13725, 136rexlimddv 3182 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ ((𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘)) ∧ 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓))) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
138137expr 448 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
139138exlimdv 2028 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑓) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14019, 139syl5bi 233 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ ω ∧ 𝑓 ∈ (𝐺𝑘))) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
141140rexlimdvaa 3179 . . . . . . . 8 ((𝜑𝑥𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
14218, 141syl5bi 233 . . . . . . 7 ((𝜑𝑥𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)))
143142rexlimdv 3177 . . . . . 6 ((𝜑𝑥𝑋) → (∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅ → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
144143expimpd 445 . . . . 5 (𝜑 → ((𝑥𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑥) ∩ 𝒫 𝑓) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
14512, 144syl5bi 233 . . . 4 (𝜑 → (𝑥𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
146145ralrimiv 3112 . . 3 (𝜑 → ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅)
147 pweq 4320 . . . . . . 7 (𝑜 = 𝑆 → 𝒫 𝑜 = 𝒫 𝑆)
148147ineq2d 3978 . . . . . 6 (𝑜 = 𝑆 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑆))
149148neeq1d 2996 . . . . 5 (𝑜 = 𝑆 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
150149raleqbi1dv 3294 . . . 4 (𝑜 = 𝑆 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
151 neibastop1.4 . . . 4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
152150, 151elrab2 3525 . . 3 (𝑆𝐽 ↔ (𝑆 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑆 ((𝐹𝑥) ∩ 𝒫 𝑆) ≠ ∅))
1537, 146, 152sylanbrc 578 . 2 (𝜑𝑆𝐽)
154 neibastop2.p . . 3 (𝜑𝑃𝑋)
155 snidg 4366 . . . . . 6 (𝑈 ∈ (𝐹𝑃) → 𝑈 ∈ {𝑈})
15667, 155syl 17 . . . . 5 (𝜑𝑈 ∈ {𝑈})
157 peano1 7287 . . . . . . 7 ∅ ∈ ω
158 fnfvelrn 6550 . . . . . . 7 ((𝐺 Fn ω ∧ ∅ ∈ ω) → (𝐺‘∅) ∈ ran 𝐺)
15916, 157, 158mp2an 683 . . . . . 6 (𝐺‘∅) ∈ ran 𝐺
16060, 159eqeltrri 2841 . . . . 5 {𝑈} ∈ ran 𝐺
161 elunii 4601 . . . . 5 ((𝑈 ∈ {𝑈} ∧ {𝑈} ∈ ran 𝐺) → 𝑈 ran 𝐺)
162156, 160, 161sylancl 580 . . . 4 (𝜑𝑈 ran 𝐺)
163 inelcm 4195 . . . . 5 ((𝑈 ∈ (𝐹𝑃) ∧ 𝑈 ∈ 𝒫 𝑈) → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
16467, 69, 163syl2anc 579 . . . 4 (𝜑 → ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅)
165 pweq 4320 . . . . . . 7 (𝑓 = 𝑈 → 𝒫 𝑓 = 𝒫 𝑈)
166165ineq2d 3978 . . . . . 6 (𝑓 = 𝑈 → ((𝐹𝑃) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑈))
167166neeq1d 2996 . . . . 5 (𝑓 = 𝑈 → (((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅))
168167rspcev 3462 . . . 4 ((𝑈 ran 𝐺 ∧ ((𝐹𝑃) ∩ 𝒫 𝑈) ≠ ∅) → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
169162, 164, 168syl2anc 579 . . 3 (𝜑 → ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅)
170 fveq2 6379 . . . . . . 7 (𝑦 = 𝑃 → (𝐹𝑦) = (𝐹𝑃))
171170ineq1d 3977 . . . . . 6 (𝑦 = 𝑃 → ((𝐹𝑦) ∩ 𝒫 𝑓) = ((𝐹𝑃) ∩ 𝒫 𝑓))
172171neeq1d 2996 . . . . 5 (𝑦 = 𝑃 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
173172rexbidv 3199 . . . 4 (𝑦 = 𝑃 → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
174173, 1elrab2 3525 . . 3 (𝑃𝑆 ↔ (𝑃𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑃) ∩ 𝒫 𝑓) ≠ ∅))
175154, 169, 174sylanbrc 578 . 2 (𝜑𝑃𝑆)
176 eluni2 4600 . . . . . . 7 (𝑓 ran 𝐺 ↔ ∃𝑧 ∈ ran 𝐺 𝑓𝑧)
177 eleq2 2833 . . . . . . . . . 10 (𝑧 = (𝐺𝑘) → (𝑓𝑧𝑓 ∈ (𝐺𝑘)))
178177rexrn 6555 . . . . . . . . 9 (𝐺 Fn ω → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘)))
17916, 178ax-mp 5 . . . . . . . 8 (∃𝑧 ∈ ran 𝐺 𝑓𝑧 ↔ ∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘))
180105adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦𝑋) → 𝐺:ω⟶𝒫 𝒫 𝑈)
181180ffvelrnda 6553 . . . . . . . . . . . . . . . 16 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ∈ 𝒫 𝒫 𝑈)
182181elpwid 4329 . . . . . . . . . . . . . . 15 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝐺𝑘) ⊆ 𝒫 𝑈)
183182sselda 3763 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → 𝑓 ∈ 𝒫 𝑈)
184183adantrr 708 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓 ∈ 𝒫 𝑈)
185184elpwid 4329 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑈)
186 neibastop2.u . . . . . . . . . . . . 13 (𝜑𝑈𝑁)
187186ad3antrrr 721 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑈𝑁)
188185, 187sstrd 3773 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑓𝑁)
189 n0 4097 . . . . . . . . . . . . 13 (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓))
190 elin 3960 . . . . . . . . . . . . . . 15 (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) ↔ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))
191 simprrr 800 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ 𝒫 𝑓)
192191elpwid 4329 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣𝑓)
193 simpllr 793 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑋)
194 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥))) → 𝑥𝑣)
195194expr 448 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝑋) → (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
196195ralrimiva 3113 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
197196ad3antrrr 721 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → ∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣))
198 simprrl 799 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑣 ∈ (𝐹𝑦))
199 fveq2 6379 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
200199eleq2d 2830 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑣 ∈ (𝐹𝑥) ↔ 𝑣 ∈ (𝐹𝑦)))
201 elequ1 2162 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥𝑣𝑦𝑣))
202200, 201imbi12d 335 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → ((𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) ↔ (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
203202rspcv 3458 . . . . . . . . . . . . . . . . . 18 (𝑦𝑋 → (∀𝑥𝑋 (𝑣 ∈ (𝐹𝑥) → 𝑥𝑣) → (𝑣 ∈ (𝐹𝑦) → 𝑦𝑣)))
204193, 197, 198, 203syl3c 66 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑣)
205192, 204sseldd 3764 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ (𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓))) → 𝑦𝑓)
206205expr 448 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → ((𝑣 ∈ (𝐹𝑦) ∧ 𝑣 ∈ 𝒫 𝑓) → 𝑦𝑓))
207190, 206syl5bi 233 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
208207exlimdv 2028 . . . . . . . . . . . . 13 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (∃𝑣 𝑣 ∈ ((𝐹𝑦) ∩ 𝒫 𝑓) → 𝑦𝑓))
209189, 208syl5bi 233 . . . . . . . . . . . 12 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ 𝑓 ∈ (𝐺𝑘)) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑓))
210209impr 446 . . . . . . . . . . 11 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑓)
211188, 210sseldd 3764 . . . . . . . . . 10 ((((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) ∧ (𝑓 ∈ (𝐺𝑘) ∧ ((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅)) → 𝑦𝑁)
212211exp32 411 . . . . . . . . 9 (((𝜑𝑦𝑋) ∧ 𝑘 ∈ ω) → (𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
213212rexlimdva 3178 . . . . . . . 8 ((𝜑𝑦𝑋) → (∃𝑘 ∈ ω 𝑓 ∈ (𝐺𝑘) → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
214179, 213syl5bi 233 . . . . . . 7 ((𝜑𝑦𝑋) → (∃𝑧 ∈ ran 𝐺 𝑓𝑧 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
215176, 214syl5bi 233 . . . . . 6 ((𝜑𝑦𝑋) → (𝑓 ran 𝐺 → (((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁)))
216215rexlimdv 3177 . . . . 5 ((𝜑𝑦𝑋) → (∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅ → 𝑦𝑁))
2172163impia 1145 . . . 4 ((𝜑𝑦𝑋 ∧ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅) → 𝑦𝑁)
218217rabssdv 3844 . . 3 (𝜑 → {𝑦𝑋 ∣ ∃𝑓 ran 𝐺((𝐹𝑦) ∩ 𝒫 𝑓) ≠ ∅} ⊆ 𝑁)
2191, 218syl5eqss 3811 . 2 (𝜑𝑆𝑁)
220 eleq2 2833 . . . 4 (𝑢 = 𝑆 → (𝑃𝑢𝑃𝑆))
221 sseq1 3788 . . . 4 (𝑢 = 𝑆 → (𝑢𝑁𝑆𝑁))
222220, 221anbi12d 624 . . 3 (𝑢 = 𝑆 → ((𝑃𝑢𝑢𝑁) ↔ (𝑃𝑆𝑆𝑁)))
223222rspcev 3462 . 2 ((𝑆𝐽 ∧ (𝑃𝑆𝑆𝑁)) → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
224153, 175, 219, 223syl12anc 865 1 (𝜑 → ∃𝑢𝐽 (𝑃𝑢𝑢𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3731  cin 3733  wss 3734  c0 4081  𝒫 cpw 4317  {csn 4336   cuni 4596   ciun 4678  cmpt 4890  ran crn 5280  cres 5281  suc csuc 5912   Fn wfn 6065  wf 6066  cfv 6070  ωcom 7267  reccrdg 7713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-om 7268  df-wrecs 7614  df-recs 7676  df-rdg 7714
This theorem is referenced by:  neibastop2  32820
  Copyright terms: Public domain W3C validator