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

Theorem neibastop1 32950
 Description: A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard's General Topology. (Contributed by Jeff Hankins, 8-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
neibastop1.1 (𝜑𝑋𝑉)
neibastop1.2 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
neibastop1.3 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
neibastop1.4 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
Assertion
Ref Expression
neibastop1 (𝜑𝐽 ∈ (TopOn‘𝑋))
Distinct variable groups:   𝑥,𝑣,𝐽   𝑣,𝑜,𝑤,𝑥,𝐹   𝜑,𝑜,𝑣,𝑤,𝑥   𝑜,𝑋,𝑣,𝑤,𝑥
Allowed substitution hints:   𝐽(𝑤,𝑜)   𝑉(𝑥,𝑤,𝑣,𝑜)

Proof of Theorem neibastop1
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 479 . . . . . . . . 9 ((𝜑𝑦𝐽) → 𝑦𝐽)
2 neibastop1.4 . . . . . . . . . 10 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
3 ssrab2 3908 . . . . . . . . . 10 {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋
42, 3eqsstri 3854 . . . . . . . . 9 𝐽 ⊆ 𝒫 𝑋
51, 4syl6ss 3833 . . . . . . . 8 ((𝜑𝑦𝐽) → 𝑦 ⊆ 𝒫 𝑋)
6 sspwuni 4847 . . . . . . . 8 (𝑦 ⊆ 𝒫 𝑋 𝑦𝑋)
75, 6sylib 210 . . . . . . 7 ((𝜑𝑦𝐽) → 𝑦𝑋)
8 vuniex 7233 . . . . . . . 8 𝑦 ∈ V
98elpw 4385 . . . . . . 7 ( 𝑦 ∈ 𝒫 𝑋 𝑦𝑋)
107, 9sylibr 226 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4677 . . . . . . . 8 (𝑥 𝑦 ↔ ∃𝑧𝑦 𝑥𝑧)
12 elssuni 4704 . . . . . . . . . . . . 13 (𝑧𝑦𝑧 𝑦)
1312ad2antrl 718 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧 𝑦)
14 sspwb 5151 . . . . . . . . . . . 12 (𝑧 𝑦 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑦)
1513, 14sylib 210 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝒫 𝑧 ⊆ 𝒫 𝑦)
16 sslin 4059 . . . . . . . . . . 11 (𝒫 𝑧 ⊆ 𝒫 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
1715, 16syl 17 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
181sselda 3821 . . . . . . . . . . . . 13 (((𝜑𝑦𝐽) ∧ 𝑧𝑦) → 𝑧𝐽)
1918adantrr 707 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧𝐽)
20 pweq 4382 . . . . . . . . . . . . . . . . 17 (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧)
2120ineq2d 4037 . . . . . . . . . . . . . . . 16 (𝑜 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑧))
2221neeq1d 3028 . . . . . . . . . . . . . . 15 (𝑜 = 𝑧 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2322raleqbi1dv 3328 . . . . . . . . . . . . . 14 (𝑜 = 𝑧 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2423, 2elrab2 3576 . . . . . . . . . . . . 13 (𝑧𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2524simprbi 492 . . . . . . . . . . . 12 (𝑧𝐽 → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
2619, 25syl 17 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
27 simprr 763 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑥𝑧)
28 rsp 3111 . . . . . . . . . . 11 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2926, 27, 28sylc 65 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
30 ssn0 4202 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3117, 29, 30syl2anc 579 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3231rexlimdvaa 3214 . . . . . . . 8 ((𝜑𝑦𝐽) → (∃𝑧𝑦 𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3311, 32syl5bi 234 . . . . . . 7 ((𝜑𝑦𝐽) → (𝑥 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3433ralrimiv 3147 . . . . . 6 ((𝜑𝑦𝐽) → ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
35 pweq 4382 . . . . . . . . . 10 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
3635ineq2d 4037 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
3736neeq1d 3028 . . . . . . . 8 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3837raleqbi1dv 3328 . . . . . . 7 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3938, 2elrab2 3576 . . . . . 6 ( 𝑦𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4010, 34, 39sylanbrc 578 . . . . 5 ((𝜑𝑦𝐽) → 𝑦𝐽)
4140ex 403 . . . 4 (𝜑 → (𝑦𝐽 𝑦𝐽))
4241alrimiv 1970 . . 3 (𝜑 → ∀𝑦(𝑦𝐽 𝑦𝐽))
43 pweq 4382 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
4443ineq2d 4037 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
4544neeq1d 3028 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4645raleqbi1dv 3328 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4746, 2elrab2 3576 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4847, 24anbi12i 620 . . . . . 6 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
49 an4 646 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
5048, 49bitri 267 . . . . 5 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
51 inss1 4053 . . . . . . . . . 10 (𝑦𝑧) ⊆ 𝑦
52 elpwi 4389 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
5351, 52syl5ss 3832 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 → (𝑦𝑧) ⊆ 𝑋)
5453ad2antrl 718 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (𝑦𝑧) ⊆ 𝑋)
5554adantrr 707 . . . . . . 7 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ⊆ 𝑋)
56 vex 3401 . . . . . . . . 9 𝑦 ∈ V
5756inex1 5038 . . . . . . . 8 (𝑦𝑧) ∈ V
5857elpw 4385 . . . . . . 7 ((𝑦𝑧) ∈ 𝒫 𝑋 ↔ (𝑦𝑧) ⊆ 𝑋)
5955, 58sylibr 226 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝒫 𝑋)
60 ssralv 3885 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
6151, 60ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
62 inss2 4054 . . . . . . . . . . 11 (𝑦𝑧) ⊆ 𝑧
63 ssralv 3885 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑧 → (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6462, 63ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
6561, 64anim12i 606 . . . . . . . . 9 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
66 r19.26 3250 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6765, 66sylibr 226 . . . . . . . 8 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
68 n0 4159 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
69 n0 4159 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7068, 69anbi12i 620 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
71 exdistrv 1998 . . . . . . . . . . 11 (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
72 inss2 4054 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦
73 simprl 761 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
7472, 73sseldi 3819 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦)
7574elpwid 4391 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣𝑦)
76 inss2 4054 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
77 simprr 763 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7876, 77sseldi 3819 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
7978elpwid 4391 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤𝑧)
80 ss2in 4061 . . . . . . . . . . . . . . . . 17 ((𝑣𝑦𝑤𝑧) → (𝑣𝑤) ⊆ (𝑦𝑧))
8175, 79, 80syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑣𝑤) ⊆ (𝑦𝑧))
82 sspwb 5151 . . . . . . . . . . . . . . . 16 ((𝑣𝑤) ⊆ (𝑦𝑧) ↔ 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
8381, 82sylib 210 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
84 sslin 4059 . . . . . . . . . . . . . . 15 (𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
8583, 84syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
86 simplll 765 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝜑)
8754ad2antrr 716 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑦𝑧) ⊆ 𝑋)
88 simplr 759 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦𝑧))
8987, 88sseldd 3822 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥𝑋)
90 inss1 4053 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹𝑥)
9190, 73sseldi 3819 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹𝑥))
92 inss1 4053 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹𝑥)
9392, 77sseldi 3819 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹𝑥))
94 neibastop1.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
9586, 89, 91, 93, 94syl13anc 1440 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
96 ssn0 4202 . . . . . . . . . . . . . 14 ((((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ∧ ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9785, 95, 96syl2anc 579 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9897ex 403 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9998exlimdvv 1977 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10071, 99syl5bir 235 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10170, 100syl5bi 234 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
102101ralimdva 3144 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10367, 102syl5 34 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
104103impr 448 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
105 pweq 4382 . . . . . . . . . 10 (𝑜 = (𝑦𝑧) → 𝒫 𝑜 = 𝒫 (𝑦𝑧))
106105ineq2d 4037 . . . . . . . . 9 (𝑜 = (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
107106neeq1d 3028 . . . . . . . 8 (𝑜 = (𝑦𝑧) → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
108107raleqbi1dv 3328 . . . . . . 7 (𝑜 = (𝑦𝑧) → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
109108, 2elrab2 3576 . . . . . 6 ((𝑦𝑧) ∈ 𝐽 ↔ ((𝑦𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
11059, 104, 109sylanbrc 578 . . . . 5 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝐽)
11150, 110sylan2b 587 . . . 4 ((𝜑 ∧ (𝑦𝐽𝑧𝐽)) → (𝑦𝑧) ∈ 𝐽)
112111ralrimivva 3153 . . 3 (𝜑 → ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)
113 neibastop1.1 . . . . . 6 (𝜑𝑋𝑉)
114 sspwuni 4847 . . . . . . . 8 (𝐽 ⊆ 𝒫 𝑋 𝐽𝑋)
1154, 114mpbi 222 . . . . . . 7 𝐽𝑋
116115a1i 11 . . . . . 6 (𝜑 𝐽𝑋)
117113, 116ssexd 5044 . . . . 5 (𝜑 𝐽 ∈ V)
118 uniexb 7252 . . . . 5 (𝐽 ∈ V ↔ 𝐽 ∈ V)
119117, 118sylibr 226 . . . 4 (𝜑𝐽 ∈ V)
120 istopg 21118 . . . 4 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
121119, 120syl 17 . . 3 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
12242, 112, 121mpbir2and 703 . 2 (𝜑𝐽 ∈ Top)
123 pwidg 4394 . . . . . 6 (𝑋𝑉𝑋 ∈ 𝒫 𝑋)
124113, 123syl 17 . . . . 5 (𝜑𝑋 ∈ 𝒫 𝑋)
125 neibastop1.2 . . . . . . . . . 10 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
126125ffvelrnda 6625 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}))
127 eldifi 3955 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝒫 𝑋)
128 elpwi 4389 . . . . . . . . 9 ((𝐹𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹𝑥) ⊆ 𝒫 𝑋)
129126, 127, 1283syl 18 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐹𝑥) ⊆ 𝒫 𝑋)
130 df-ss 3806 . . . . . . . 8 ((𝐹𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
131129, 130sylib 210 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
132 eldifsni 4553 . . . . . . . 8 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
133126, 132syl 17 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ≠ ∅)
134131, 133eqnetrd 3036 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
135134ralrimiva 3148 . . . . 5 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
136 pweq 4382 . . . . . . . . 9 (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋)
137136ineq2d 4037 . . . . . . . 8 (𝑜 = 𝑋 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑋))
138137neeq1d 3028 . . . . . . 7 (𝑜 = 𝑋 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
139138raleqbi1dv 3328 . . . . . 6 (𝑜 = 𝑋 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
140139, 2elrab2 3576 . . . . 5 (𝑋𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
141124, 135, 140sylanbrc 578 . . . 4 (𝜑𝑋𝐽)
142 elssuni 4704 . . . 4 (𝑋𝐽𝑋 𝐽)
143141, 142syl 17 . . 3 (𝜑𝑋 𝐽)
144143, 116eqssd 3838 . 2 (𝜑𝑋 = 𝐽)
145 istopon 21135 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
146122, 144, 145sylanbrc 578 1 (𝜑𝐽 ∈ (TopOn‘𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071  ∀wal 1599   = wceq 1601  ∃wex 1823   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  {crab 3094  Vcvv 3398   ∖ cdif 3789   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  𝒫 cpw 4379  {csn 4398  ∪ cuni 4673  ⟶wf 6133  ‘cfv 6137  Topctop 21116  TopOnctopon 21133 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145  df-top 21117  df-topon 21134 This theorem is referenced by:  neibastop2  32952  neibastop3  32953
 Copyright terms: Public domain W3C validator