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

Theorem neibastop3 34863
Description: The topology generated by a neighborhood base is unique. (Contributed by Jeff Hankins, 16-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
neibastop1.1 (πœ‘ β†’ 𝑋 ∈ 𝑉)
neibastop1.2 (πœ‘ β†’ 𝐹:π‘‹βŸΆ(𝒫 𝒫 𝑋 βˆ– {βˆ…}))
neibastop1.3 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯) ∧ 𝑀 ∈ (πΉβ€˜π‘₯))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
neibastop1.4 𝐽 = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…}
neibastop1.5 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ π‘₯ ∈ 𝑣)
neibastop1.6 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
Assertion
Ref Expression
neibastop3 (πœ‘ β†’ βˆƒ!𝑗 ∈ (TopOnβ€˜π‘‹)βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
Distinct variable groups:   𝑑,𝑛,𝑣,𝑦,𝑗,π‘₯   𝑗,𝐽   π‘₯,𝑛,𝐽,𝑣,𝑦   𝑑,π‘œ,𝑣,𝑀,π‘₯,𝑦,𝑗,𝐹,𝑛   πœ‘,𝑗,𝑛,π‘œ,𝑑,𝑣,𝑀,π‘₯,𝑦   𝑗,𝑋,𝑛,π‘œ,𝑑,𝑣,𝑀,π‘₯,𝑦
Allowed substitution hints:   𝐽(𝑀,𝑑,π‘œ)   𝑉(π‘₯,𝑦,𝑀,𝑣,𝑑,𝑗,𝑛,π‘œ)

Proof of Theorem neibastop3
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 neibastop1.1 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝑉)
2 neibastop1.2 . . . 4 (πœ‘ β†’ 𝐹:π‘‹βŸΆ(𝒫 𝒫 𝑋 βˆ– {βˆ…}))
3 neibastop1.3 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯) ∧ 𝑀 ∈ (πΉβ€˜π‘₯))) β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 (𝑣 ∩ 𝑀)) β‰  βˆ…)
4 neibastop1.4 . . . 4 𝐽 = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…}
51, 2, 3, 4neibastop1 34860 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
6 neibastop1.5 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ π‘₯ ∈ 𝑣)
7 neibastop1.6 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
81, 2, 3, 4, 6, 7neibastop2 34862 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ (𝑛 ∈ ((neiβ€˜π½)β€˜{𝑧}) ↔ (𝑛 βŠ† 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)))
9 velpw 4570 . . . . . . . . 9 (𝑛 ∈ 𝒫 𝑋 ↔ 𝑛 βŠ† 𝑋)
109anbi1i 625 . . . . . . . 8 ((𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…) ↔ (𝑛 βŠ† 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…))
118, 10bitr4di 289 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ (𝑛 ∈ ((neiβ€˜π½)β€˜{𝑧}) ↔ (𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)))
1211abbi2dv 2872 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∣ (𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)})
13 df-rab 3411 . . . . . 6 {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…} = {𝑛 ∣ (𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)}
1412, 13eqtr4di 2795 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
1514ralrimiva 3144 . . . 4 (πœ‘ β†’ βˆ€π‘§ ∈ 𝑋 ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
16 sneq 4601 . . . . . . 7 (π‘₯ = 𝑧 β†’ {π‘₯} = {𝑧})
1716fveq2d 6851 . . . . . 6 (π‘₯ = 𝑧 β†’ ((neiβ€˜π½)β€˜{π‘₯}) = ((neiβ€˜π½)β€˜{𝑧}))
18 fveq2 6847 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘§))
1918ineq1d 4176 . . . . . . . 8 (π‘₯ = 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) = ((πΉβ€˜π‘§) ∩ 𝒫 𝑛))
2019neeq1d 3004 . . . . . . 7 (π‘₯ = 𝑧 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ… ↔ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…))
2120rabbidv 3418 . . . . . 6 (π‘₯ = 𝑧 β†’ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
2217, 21eqeq12d 2753 . . . . 5 (π‘₯ = 𝑧 β†’ (((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…}))
2322cbvralvw 3228 . . . 4 (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ βˆ€π‘§ ∈ 𝑋 ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
2415, 23sylibr 233 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
25 toponuni 22279 . . . . . . . . . 10 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝑗)
26 eqimss2 4006 . . . . . . . . . 10 (𝑋 = βˆͺ 𝑗 β†’ βˆͺ 𝑗 βŠ† 𝑋)
2725, 26syl 17 . . . . . . . . 9 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ βˆͺ 𝑗 βŠ† 𝑋)
28 sspwuni 5065 . . . . . . . . 9 (𝑗 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝑗 βŠ† 𝑋)
2927, 28sylibr 233 . . . . . . . 8 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ 𝑗 βŠ† 𝒫 𝑋)
3029ad2antlr 726 . . . . . . 7 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 βŠ† 𝒫 𝑋)
31 sseqin2 4180 . . . . . . 7 (𝑗 βŠ† 𝒫 𝑋 ↔ (𝒫 𝑋 ∩ 𝑗) = 𝑗)
3230, 31sylib 217 . . . . . 6 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ (𝒫 𝑋 ∩ 𝑗) = 𝑗)
33 topontop 22278 . . . . . . . . . . 11 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ 𝑗 ∈ Top)
3433ad3antlr 730 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ 𝑗 ∈ Top)
35 eltop2 22341 . . . . . . . . . 10 (𝑗 ∈ Top β†’ (π‘œ ∈ 𝑗 ↔ βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
3634, 35syl 17 . . . . . . . . 9 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (π‘œ ∈ 𝑗 ↔ βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
37 elpwi 4572 . . . . . . . . . . . . . . 15 (π‘œ ∈ 𝒫 𝑋 β†’ π‘œ βŠ† 𝑋)
38 ssralv 4015 . . . . . . . . . . . . . . 15 (π‘œ βŠ† 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
3937, 38syl 17 . . . . . . . . . . . . . 14 (π‘œ ∈ 𝒫 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
4039adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
41 simprr 772 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
4241eleq2d 2824 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ π‘œ ∈ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
4333ad3antlr 730 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ 𝑗 ∈ Top)
4425adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) β†’ 𝑋 = βˆͺ 𝑗)
4544sseq2d 3981 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) β†’ (π‘œ βŠ† 𝑋 ↔ π‘œ βŠ† βˆͺ 𝑗))
4645biimpa 478 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ βŠ† 𝑋) β†’ π‘œ βŠ† βˆͺ 𝑗)
4737, 46sylan2 594 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ π‘œ βŠ† βˆͺ 𝑗)
4847sselda 3949 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ π‘₯ ∈ π‘œ) β†’ π‘₯ ∈ βˆͺ 𝑗)
4948adantrr 716 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ π‘₯ ∈ βˆͺ 𝑗)
5047adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ π‘œ βŠ† βˆͺ 𝑗)
51 eqid 2737 . . . . . . . . . . . . . . . . . . 19 βˆͺ 𝑗 = βˆͺ 𝑗
5251isneip 22472 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ Top ∧ π‘₯ ∈ βˆͺ 𝑗) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ (π‘œ βŠ† βˆͺ 𝑗 ∧ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ))))
5352baibd 541 . . . . . . . . . . . . . . . . 17 (((𝑗 ∈ Top ∧ π‘₯ ∈ βˆͺ 𝑗) ∧ π‘œ βŠ† βˆͺ 𝑗) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
5443, 49, 50, 53syl21anc 837 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
55 pweq 4579 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = π‘œ β†’ 𝒫 𝑛 = 𝒫 π‘œ)
5655ineq2d 4177 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘œ β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) = ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ))
5756neeq1d 3004 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘œ β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
5857elrab3 3651 . . . . . . . . . . . . . . . . 17 (π‘œ ∈ 𝒫 𝑋 β†’ (π‘œ ∈ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
5958ad2antlr 726 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (π‘œ ∈ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6042, 54, 593bitr3d 309 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6160expr 458 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ π‘₯ ∈ π‘œ) β†’ (((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…)))
6261ralimdva 3165 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…)))
6340, 62syld 47 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…)))
6463imp 408 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6564an32s 651 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
66 ralbi 3107 . . . . . . . . . 10 (βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…) β†’ (βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6765, 66syl 17 . . . . . . . . 9 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6836, 67bitrd 279 . . . . . . . 8 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (π‘œ ∈ 𝑗 ↔ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6968rabbi2dva 4182 . . . . . . 7 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ (𝒫 𝑋 ∩ 𝑗) = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…})
7069, 4eqtr4di 2795 . . . . . 6 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ (𝒫 𝑋 ∩ 𝑗) = 𝐽)
7132, 70eqtr3d 2779 . . . . 5 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽)
7271expl 459 . . . 4 (πœ‘ β†’ ((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽))
7372alrimiv 1931 . . 3 (πœ‘ β†’ βˆ€π‘—((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽))
74 eleq1 2826 . . . . 5 (𝑗 = 𝐽 β†’ (𝑗 ∈ (TopOnβ€˜π‘‹) ↔ 𝐽 ∈ (TopOnβ€˜π‘‹)))
75 fveq2 6847 . . . . . . . 8 (𝑗 = 𝐽 β†’ (neiβ€˜π‘—) = (neiβ€˜π½))
7675fveq1d 6849 . . . . . . 7 (𝑗 = 𝐽 β†’ ((neiβ€˜π‘—)β€˜{π‘₯}) = ((neiβ€˜π½)β€˜{π‘₯}))
7776eqeq1d 2739 . . . . . 6 (𝑗 = 𝐽 β†’ (((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
7877ralbidv 3175 . . . . 5 (𝑗 = 𝐽 β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
7974, 78anbi12d 632 . . . 4 (𝑗 = 𝐽 β†’ ((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ↔ (𝐽 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})))
8079eqeu 3669 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (𝐽 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ βˆ€π‘—((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽)) β†’ βˆƒ!𝑗(𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
815, 5, 24, 73, 80syl121anc 1376 . 2 (πœ‘ β†’ βˆƒ!𝑗(𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
82 df-reu 3357 . 2 (βˆƒ!𝑗 ∈ (TopOnβ€˜π‘‹)βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ βˆƒ!𝑗(𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
8381, 82sylibr 233 1 (πœ‘ β†’ βˆƒ!𝑗 ∈ (TopOnβ€˜π‘‹)βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542   ∈ wcel 2107  βˆƒ!weu 2567  {cab 2714   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  βˆƒ!wreu 3354  {crab 3410   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870  βŸΆwf 6497  β€˜cfv 6501  Topctop 22258  TopOnctopon 22275  neicnei 22464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-topgen 17332  df-top 22259  df-topon 22276  df-nei 22465
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator