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

Theorem neibastop1 33732
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 488 . . . . . . . . 9 ((𝜑𝑦𝐽) → 𝑦𝐽)
2 neibastop1.4 . . . . . . . . . 10 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅}
3 ssrab2 4041 . . . . . . . . . 10 {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋
42, 3eqsstri 3986 . . . . . . . . 9 𝐽 ⊆ 𝒫 𝑋
51, 4sstrdi 3964 . . . . . . . 8 ((𝜑𝑦𝐽) → 𝑦 ⊆ 𝒫 𝑋)
6 sspwuni 5008 . . . . . . . 8 (𝑦 ⊆ 𝒫 𝑋 𝑦𝑋)
75, 6sylib 221 . . . . . . 7 ((𝜑𝑦𝐽) → 𝑦𝑋)
8 vuniex 7455 . . . . . . . 8 𝑦 ∈ V
98elpw 4525 . . . . . . 7 ( 𝑦 ∈ 𝒫 𝑋 𝑦𝑋)
107, 9sylibr 237 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4828 . . . . . . . 8 (𝑥 𝑦 ↔ ∃𝑧𝑦 𝑥𝑧)
12 elssuni 4854 . . . . . . . . . . . . 13 (𝑧𝑦𝑧 𝑦)
1312ad2antrl 727 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧 𝑦)
1413sspwd 4536 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝒫 𝑧 ⊆ 𝒫 𝑦)
15 sslin 4195 . . . . . . . . . . 11 (𝒫 𝑧 ⊆ 𝒫 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
1614, 15syl 17 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
171sselda 3952 . . . . . . . . . . . . 13 (((𝜑𝑦𝐽) ∧ 𝑧𝑦) → 𝑧𝐽)
1817adantrr 716 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧𝐽)
19 pweq 4537 . . . . . . . . . . . . . . . . 17 (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧)
2019ineq2d 4173 . . . . . . . . . . . . . . . 16 (𝑜 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑧))
2120neeq1d 3073 . . . . . . . . . . . . . . 15 (𝑜 = 𝑧 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2221raleqbi1dv 3395 . . . . . . . . . . . . . 14 (𝑜 = 𝑧 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2322, 2elrab2 3669 . . . . . . . . . . . . 13 (𝑧𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2423simprbi 500 . . . . . . . . . . . 12 (𝑧𝐽 → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
2518, 24syl 17 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
26 simprr 772 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑥𝑧)
27 rsp 3200 . . . . . . . . . . 11 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2825, 26, 27sylc 65 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
29 ssn0 4336 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3016, 28, 29syl2anc 587 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3130rexlimdvaa 3278 . . . . . . . 8 ((𝜑𝑦𝐽) → (∃𝑧𝑦 𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3211, 31syl5bi 245 . . . . . . 7 ((𝜑𝑦𝐽) → (𝑥 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3332ralrimiv 3176 . . . . . 6 ((𝜑𝑦𝐽) → ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
34 pweq 4537 . . . . . . . . . 10 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
3534ineq2d 4173 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
3635neeq1d 3073 . . . . . . . 8 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3736raleqbi1dv 3395 . . . . . . 7 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3837, 2elrab2 3669 . . . . . 6 ( 𝑦𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3910, 33, 38sylanbrc 586 . . . . 5 ((𝜑𝑦𝐽) → 𝑦𝐽)
4039ex 416 . . . 4 (𝜑 → (𝑦𝐽 𝑦𝐽))
4140alrimiv 1929 . . 3 (𝜑 → ∀𝑦(𝑦𝐽 𝑦𝐽))
42 pweq 4537 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
4342ineq2d 4173 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
4443neeq1d 3073 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4544raleqbi1dv 3395 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4645, 2elrab2 3669 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4746, 23anbi12i 629 . . . . . 6 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
48 an4 655 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
4947, 48bitri 278 . . . . 5 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
50 inss1 4189 . . . . . . . . . 10 (𝑦𝑧) ⊆ 𝑦
51 elpwi 4530 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
5250, 51sstrid 3963 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 → (𝑦𝑧) ⊆ 𝑋)
5352ad2antrl 727 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (𝑦𝑧) ⊆ 𝑋)
5453adantrr 716 . . . . . . 7 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ⊆ 𝑋)
55 vex 3483 . . . . . . . . 9 𝑦 ∈ V
5655inex1 5207 . . . . . . . 8 (𝑦𝑧) ∈ V
5756elpw 4525 . . . . . . 7 ((𝑦𝑧) ∈ 𝒫 𝑋 ↔ (𝑦𝑧) ⊆ 𝑋)
5854, 57sylibr 237 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝒫 𝑋)
59 ssralv 4018 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
6050, 59ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
61 inss2 4190 . . . . . . . . . . 11 (𝑦𝑧) ⊆ 𝑧
62 ssralv 4018 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑧 → (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6361, 62ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
6460, 63anim12i 615 . . . . . . . . 9 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
65 r19.26 3165 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6664, 65sylibr 237 . . . . . . . 8 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
67 n0 4292 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
68 n0 4292 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
6967, 68anbi12i 629 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
70 exdistrv 1957 . . . . . . . . . . 11 (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
71 inss2 4190 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦
72 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
7371, 72sseldi 3950 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦)
7473elpwid 4532 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣𝑦)
75 inss2 4190 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
76 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7775, 76sseldi 3950 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
7877elpwid 4532 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤𝑧)
79 ss2in 4197 . . . . . . . . . . . . . . . . 17 ((𝑣𝑦𝑤𝑧) → (𝑣𝑤) ⊆ (𝑦𝑧))
8074, 78, 79syl2anc 587 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑣𝑤) ⊆ (𝑦𝑧))
8180sspwd 4536 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
82 sslin 4195 . . . . . . . . . . . . . . 15 (𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
8381, 82syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
84 simplll 774 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝜑)
8553ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑦𝑧) ⊆ 𝑋)
86 simplr 768 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦𝑧))
8785, 86sseldd 3953 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥𝑋)
88 inss1 4189 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹𝑥)
8988, 72sseldi 3950 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹𝑥))
90 inss1 4189 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹𝑥)
9190, 76sseldi 3950 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹𝑥))
92 neibastop1.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
9384, 87, 89, 91, 92syl13anc 1369 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
94 ssn0 4336 . . . . . . . . . . . . . 14 ((((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ∧ ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9583, 93, 94syl2anc 587 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9695ex 416 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9796exlimdvv 1936 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9870, 97syl5bir 246 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9969, 98syl5bi 245 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10099ralimdva 3172 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10166, 100syl5 34 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
102101impr 458 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
103 pweq 4537 . . . . . . . . . 10 (𝑜 = (𝑦𝑧) → 𝒫 𝑜 = 𝒫 (𝑦𝑧))
104103ineq2d 4173 . . . . . . . . 9 (𝑜 = (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
105104neeq1d 3073 . . . . . . . 8 (𝑜 = (𝑦𝑧) → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
106105raleqbi1dv 3395 . . . . . . 7 (𝑜 = (𝑦𝑧) → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
107106, 2elrab2 3669 . . . . . 6 ((𝑦𝑧) ∈ 𝐽 ↔ ((𝑦𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10858, 102, 107sylanbrc 586 . . . . 5 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝐽)
10949, 108sylan2b 596 . . . 4 ((𝜑 ∧ (𝑦𝐽𝑧𝐽)) → (𝑦𝑧) ∈ 𝐽)
110109ralrimivva 3186 . . 3 (𝜑 → ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)
111 neibastop1.1 . . . . . 6 (𝜑𝑋𝑉)
112 sspwuni 5008 . . . . . . . 8 (𝐽 ⊆ 𝒫 𝑋 𝐽𝑋)
1134, 112mpbi 233 . . . . . . 7 𝐽𝑋
114113a1i 11 . . . . . 6 (𝜑 𝐽𝑋)
115111, 114ssexd 5214 . . . . 5 (𝜑 𝐽 ∈ V)
116 uniexb 7476 . . . . 5 (𝐽 ∈ V ↔ 𝐽 ∈ V)
117115, 116sylibr 237 . . . 4 (𝜑𝐽 ∈ V)
118 istopg 21496 . . . 4 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
119117, 118syl 17 . . 3 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
12041, 110, 119mpbir2and 712 . 2 (𝜑𝐽 ∈ Top)
121 pwidg 4543 . . . . . 6 (𝑋𝑉𝑋 ∈ 𝒫 𝑋)
122111, 121syl 17 . . . . 5 (𝜑𝑋 ∈ 𝒫 𝑋)
123 neibastop1.2 . . . . . . . . . 10 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
124123ffvelrnda 6839 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}))
125 eldifi 4088 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝒫 𝑋)
126 elpwi 4530 . . . . . . . . 9 ((𝐹𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹𝑥) ⊆ 𝒫 𝑋)
127124, 125, 1263syl 18 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐹𝑥) ⊆ 𝒫 𝑋)
128 df-ss 3936 . . . . . . . 8 ((𝐹𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
129127, 128sylib 221 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
130 eldifsni 4706 . . . . . . . 8 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
131124, 130syl 17 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ≠ ∅)
132129, 131eqnetrd 3081 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
133132ralrimiva 3177 . . . . 5 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
134 pweq 4537 . . . . . . . . 9 (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋)
135134ineq2d 4173 . . . . . . . 8 (𝑜 = 𝑋 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑋))
136135neeq1d 3073 . . . . . . 7 (𝑜 = 𝑋 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
137136raleqbi1dv 3395 . . . . . 6 (𝑜 = 𝑋 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
138137, 2elrab2 3669 . . . . 5 (𝑋𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
139122, 133, 138sylanbrc 586 . . . 4 (𝜑𝑋𝐽)
140 elssuni 4854 . . . 4 (𝑋𝐽𝑋 𝐽)
141139, 140syl 17 . . 3 (𝜑𝑋 𝐽)
142141, 114eqssd 3969 . 2 (𝜑𝑋 = 𝐽)
143 istopon 21513 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
144120, 142, 143sylanbrc 586 1 (𝜑𝐽 ∈ (TopOn‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wex 1781  wcel 2115  wne 3014  wral 3133  wrex 3134  {crab 3137  Vcvv 3480  cdif 3916  cin 3918  wss 3919  c0 4275  𝒫 cpw 4521  {csn 4549   cuni 4824  wf 6339  cfv 6343  Topctop 21494  TopOnctopon 21511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-fv 6351  df-top 21495  df-topon 21512
This theorem is referenced by:  neibastop2  33734  neibastop3  33735
  Copyright terms: Public domain W3C validator