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 34203
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 3979 . . . . . . . . . 10 {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅} ⊆ 𝒫 𝑋
42, 3eqsstri 3921 . . . . . . . . 9 𝐽 ⊆ 𝒫 𝑋
51, 4sstrdi 3899 . . . . . . . 8 ((𝜑𝑦𝐽) → 𝑦 ⊆ 𝒫 𝑋)
6 sspwuni 4995 . . . . . . . 8 (𝑦 ⊆ 𝒫 𝑋 𝑦𝑋)
75, 6sylib 221 . . . . . . 7 ((𝜑𝑦𝐽) → 𝑦𝑋)
8 vuniex 7495 . . . . . . . 8 𝑦 ∈ V
98elpw 4502 . . . . . . 7 ( 𝑦 ∈ 𝒫 𝑋 𝑦𝑋)
107, 9sylibr 237 . . . . . 6 ((𝜑𝑦𝐽) → 𝑦 ∈ 𝒫 𝑋)
11 eluni2 4810 . . . . . . . 8 (𝑥 𝑦 ↔ ∃𝑧𝑦 𝑥𝑧)
12 elssuni 4838 . . . . . . . . . . . . 13 (𝑧𝑦𝑧 𝑦)
1312ad2antrl 728 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧 𝑦)
1413sspwd 4513 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝒫 𝑧 ⊆ 𝒫 𝑦)
15 sslin 4135 . . . . . . . . . . 11 (𝒫 𝑧 ⊆ 𝒫 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
1614, 15syl 17 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦))
171sselda 3887 . . . . . . . . . . . . 13 (((𝜑𝑦𝐽) ∧ 𝑧𝑦) → 𝑧𝐽)
1817adantrr 717 . . . . . . . . . . . 12 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑧𝐽)
19 pweq 4514 . . . . . . . . . . . . . . . . 17 (𝑜 = 𝑧 → 𝒫 𝑜 = 𝒫 𝑧)
2019ineq2d 4113 . . . . . . . . . . . . . . . 16 (𝑜 = 𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑧))
2120neeq1d 2994 . . . . . . . . . . . . . . 15 (𝑜 = 𝑧 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2221raleqbi1dv 3309 . . . . . . . . . . . . . 14 (𝑜 = 𝑧 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2322, 2elrab2 3596 . . . . . . . . . . . . 13 (𝑧𝐽 ↔ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2423simprbi 500 . . . . . . . . . . . 12 (𝑧𝐽 → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
2518, 24syl 17 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
26 simprr 773 . . . . . . . . . . 11 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → 𝑥𝑧)
27 rsp 3119 . . . . . . . . . . 11 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → (𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
2825, 26, 27sylc 65 . . . . . . . . . 10 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
29 ssn0 4299 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3016, 28, 29syl2anc 587 . . . . . . . . 9 (((𝜑𝑦𝐽) ∧ (𝑧𝑦𝑥𝑧)) → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
3130rexlimdvaa 3196 . . . . . . . 8 ((𝜑𝑦𝐽) → (∃𝑧𝑦 𝑥𝑧 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3211, 31syl5bi 245 . . . . . . 7 ((𝜑𝑦𝐽) → (𝑥 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3332ralrimiv 3096 . . . . . 6 ((𝜑𝑦𝐽) → ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
34 pweq 4514 . . . . . . . . . 10 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
3534ineq2d 4113 . . . . . . . . 9 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
3635neeq1d 2994 . . . . . . . 8 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3736raleqbi1dv 3309 . . . . . . 7 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3837, 2elrab2 3596 . . . . . 6 ( 𝑦𝐽 ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 𝑦((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
3910, 33, 38sylanbrc 586 . . . . 5 ((𝜑𝑦𝐽) → 𝑦𝐽)
4039ex 416 . . . 4 (𝜑 → (𝑦𝐽 𝑦𝐽))
4140alrimiv 1934 . . 3 (𝜑 → ∀𝑦(𝑦𝐽 𝑦𝐽))
42 pweq 4514 . . . . . . . . . . 11 (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
4342ineq2d 4113 . . . . . . . . . 10 (𝑜 = 𝑦 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑦))
4443neeq1d 2994 . . . . . . . . 9 (𝑜 = 𝑦 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4544raleqbi1dv 3309 . . . . . . . 8 (𝑜 = 𝑦 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4645, 2elrab2 3596 . . . . . . 7 (𝑦𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
4746, 23anbi12i 630 . . . . . 6 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
48 an4 656 . . . . . 6 (((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅) ∧ (𝑧 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
4947, 48bitri 278 . . . . 5 ((𝑦𝐽𝑧𝐽) ↔ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)))
50 inss1 4129 . . . . . . . . . 10 (𝑦𝑧) ⊆ 𝑦
51 elpwi 4507 . . . . . . . . . 10 (𝑦 ∈ 𝒫 𝑋𝑦𝑋)
5250, 51sstrid 3898 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝑋 → (𝑦𝑧) ⊆ 𝑋)
5352ad2antrl 728 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (𝑦𝑧) ⊆ 𝑋)
5453adantrr 717 . . . . . . 7 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ⊆ 𝑋)
55 vex 3404 . . . . . . . . 9 𝑦 ∈ V
5655inex1 5195 . . . . . . . 8 (𝑦𝑧) ∈ V
5756elpw 4502 . . . . . . 7 ((𝑦𝑧) ∈ 𝒫 𝑋 ↔ (𝑦𝑧) ⊆ 𝑋)
5854, 57sylibr 237 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝒫 𝑋)
59 ssralv 3953 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑦 → (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅))
6050, 59ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅)
61 inss2 4130 . . . . . . . . . . 11 (𝑦𝑧) ⊆ 𝑧
62 ssralv 3953 . . . . . . . . . . 11 ((𝑦𝑧) ⊆ 𝑧 → (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6361, 62ax-mp 5 . . . . . . . . . 10 (∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅)
6460, 63anim12i 616 . . . . . . . . 9 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
65 r19.26 3085 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
6664, 65sylibr 237 . . . . . . . 8 ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))
67 n0 4245 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
68 n0 4245 . . . . . . . . . . 11 (((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
6967, 68anbi12i 630 . . . . . . . . . 10 ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
70 exdistrv 1963 . . . . . . . . . . 11 (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) ↔ (∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)))
71 inss2 4130 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ 𝒫 𝑦
72 simprl 771 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦))
7371, 72sseldi 3885 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ 𝒫 𝑦)
7473elpwid 4509 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣𝑦)
75 inss2 4130 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ 𝒫 𝑧
76 simprr 773 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))
7775, 76sseldi 3885 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ 𝒫 𝑧)
7877elpwid 4509 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤𝑧)
79 ss2in 4137 . . . . . . . . . . . . . . . . 17 ((𝑣𝑦𝑤𝑧) → (𝑣𝑤) ⊆ (𝑦𝑧))
8074, 78, 79syl2anc 587 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑣𝑤) ⊆ (𝑦𝑧))
8180sspwd 4513 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧))
82 sslin 4135 . . . . . . . . . . . . . . 15 (𝒫 (𝑣𝑤) ⊆ 𝒫 (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
8381, 82syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
84 simplll 775 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝜑)
8553ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → (𝑦𝑧) ⊆ 𝑋)
86 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥 ∈ (𝑦𝑧))
8785, 86sseldd 3888 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑥𝑋)
88 inss1 4129 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑦) ⊆ (𝐹𝑥)
8988, 72sseldi 3885 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑣 ∈ (𝐹𝑥))
90 inss1 4129 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∩ 𝒫 𝑧) ⊆ (𝐹𝑥)
9190, 76sseldi 3885 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → 𝑤 ∈ (𝐹𝑥))
92 neibastop1.3 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑋𝑣 ∈ (𝐹𝑥) ∧ 𝑤 ∈ (𝐹𝑥))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
9384, 87, 89, 91, 92syl13anc 1373 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅)
94 ssn0 4299 . . . . . . . . . . . . . 14 ((((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ⊆ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ∧ ((𝐹𝑥) ∩ 𝒫 (𝑣𝑤)) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9583, 93, 94syl2anc 587 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) ∧ (𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧))) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
9695ex 416 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9796exlimdvv 1941 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → (∃𝑣𝑤(𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9870, 97syl5bir 246 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((∃𝑣 𝑣 ∈ ((𝐹𝑥) ∩ 𝒫 𝑦) ∧ ∃𝑤 𝑤 ∈ ((𝐹𝑥) ∩ 𝒫 𝑧)) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
9969, 98syl5bi 245 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) ∧ 𝑥 ∈ (𝑦𝑧)) → ((((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10099ralimdva 3092 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → (∀𝑥 ∈ (𝑦𝑧)(((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10166, 100syl5 34 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋)) → ((∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
102101impr 458 . . . . . 6 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
103 pweq 4514 . . . . . . . . . 10 (𝑜 = (𝑦𝑧) → 𝒫 𝑜 = 𝒫 (𝑦𝑧))
104103ineq2d 4113 . . . . . . . . 9 (𝑜 = (𝑦𝑧) → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)))
105104neeq1d 2994 . . . . . . . 8 (𝑜 = (𝑦𝑧) → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
106105raleqbi1dv 3309 . . . . . . 7 (𝑜 = (𝑦𝑧) → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
107106, 2elrab2 3596 . . . . . 6 ((𝑦𝑧) ∈ 𝐽 ↔ ((𝑦𝑧) ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ (𝑦𝑧)((𝐹𝑥) ∩ 𝒫 (𝑦𝑧)) ≠ ∅))
10858, 102, 107sylanbrc 586 . . . . 5 ((𝜑 ∧ ((𝑦 ∈ 𝒫 𝑋𝑧 ∈ 𝒫 𝑋) ∧ (∀𝑥𝑦 ((𝐹𝑥) ∩ 𝒫 𝑦) ≠ ∅ ∧ ∀𝑥𝑧 ((𝐹𝑥) ∩ 𝒫 𝑧) ≠ ∅))) → (𝑦𝑧) ∈ 𝐽)
10949, 108sylan2b 597 . . . 4 ((𝜑 ∧ (𝑦𝐽𝑧𝐽)) → (𝑦𝑧) ∈ 𝐽)
110109ralrimivva 3104 . . 3 (𝜑 → ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)
111 neibastop1.1 . . . . . 6 (𝜑𝑋𝑉)
112 sspwuni 4995 . . . . . . . 8 (𝐽 ⊆ 𝒫 𝑋 𝐽𝑋)
1134, 112mpbi 233 . . . . . . 7 𝐽𝑋
114113a1i 11 . . . . . 6 (𝜑 𝐽𝑋)
115111, 114ssexd 5202 . . . . 5 (𝜑 𝐽 ∈ V)
116 uniexb 7517 . . . . 5 (𝐽 ∈ V ↔ 𝐽 ∈ V)
117115, 116sylibr 237 . . . 4 (𝜑𝐽 ∈ V)
118 istopg 21658 . . . 4 (𝐽 ∈ V → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
119117, 118syl 17 . . 3 (𝜑 → (𝐽 ∈ Top ↔ (∀𝑦(𝑦𝐽 𝑦𝐽) ∧ ∀𝑦𝐽𝑧𝐽 (𝑦𝑧) ∈ 𝐽)))
12041, 110, 119mpbir2and 713 . 2 (𝜑𝐽 ∈ Top)
121 pwidg 4520 . . . . . 6 (𝑋𝑉𝑋 ∈ 𝒫 𝑋)
122111, 121syl 17 . . . . 5 (𝜑𝑋 ∈ 𝒫 𝑋)
123 neibastop1.2 . . . . . . . . . 10 (𝜑𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
124123ffvelrnda 6873 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}))
125 eldifi 4027 . . . . . . . . 9 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ∈ 𝒫 𝒫 𝑋)
126 elpwi 4507 . . . . . . . . 9 ((𝐹𝑥) ∈ 𝒫 𝒫 𝑋 → (𝐹𝑥) ⊆ 𝒫 𝑋)
127124, 125, 1263syl 18 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝐹𝑥) ⊆ 𝒫 𝑋)
128 df-ss 3870 . . . . . . . 8 ((𝐹𝑥) ⊆ 𝒫 𝑋 ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
129127, 128sylib 221 . . . . . . 7 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) = (𝐹𝑥))
130 eldifsni 4688 . . . . . . . 8 ((𝐹𝑥) ∈ (𝒫 𝒫 𝑋 ∖ {∅}) → (𝐹𝑥) ≠ ∅)
131124, 130syl 17 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐹𝑥) ≠ ∅)
132129, 131eqnetrd 3002 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
133132ralrimiva 3097 . . . . 5 (𝜑 → ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅)
134 pweq 4514 . . . . . . . . 9 (𝑜 = 𝑋 → 𝒫 𝑜 = 𝒫 𝑋)
135134ineq2d 4113 . . . . . . . 8 (𝑜 = 𝑋 → ((𝐹𝑥) ∩ 𝒫 𝑜) = ((𝐹𝑥) ∩ 𝒫 𝑋))
136135neeq1d 2994 . . . . . . 7 (𝑜 = 𝑋 → (((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
137136raleqbi1dv 3309 . . . . . 6 (𝑜 = 𝑋 → (∀𝑥𝑜 ((𝐹𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
138137, 2elrab2 3596 . . . . 5 (𝑋𝐽 ↔ (𝑋 ∈ 𝒫 𝑋 ∧ ∀𝑥𝑋 ((𝐹𝑥) ∩ 𝒫 𝑋) ≠ ∅))
139122, 133, 138sylanbrc 586 . . . 4 (𝜑𝑋𝐽)
140 elssuni 4838 . . . 4 (𝑋𝐽𝑋 𝐽)
141139, 140syl 17 . . 3 (𝜑𝑋 𝐽)
142141, 114eqssd 3904 . 2 (𝜑𝑋 = 𝐽)
143 istopon 21675 . 2 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
144120, 142, 143sylanbrc 586 1 (𝜑𝐽 ∈ (TopOn‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088  wal 1540   = wceq 1542  wex 1786  wcel 2114  wne 2935  wral 3054  wrex 3055  {crab 3058  Vcvv 3400  cdif 3850  cin 3852  wss 3853  c0 4221  𝒫 cpw 4498  {csn 4526   cuni 4806  wf 6345  cfv 6349  Topctop 21656  TopOnctopon 21673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7491
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-sbc 3686  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-iota 6307  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-top 21657  df-topon 21674
This theorem is referenced by:  neibastop2  34205  neibastop3  34206
  Copyright terms: Public domain W3C validator