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 35551
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 35548 . . 3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
6 neibastop1.5 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ π‘₯ ∈ 𝑣)
7 neibastop1.6 . . . . . . . . 9 ((πœ‘ ∧ (π‘₯ ∈ 𝑋 ∧ 𝑣 ∈ (πΉβ€˜π‘₯))) β†’ βˆƒπ‘‘ ∈ (πΉβ€˜π‘₯)βˆ€π‘¦ ∈ 𝑑 ((πΉβ€˜π‘¦) ∩ 𝒫 𝑣) β‰  βˆ…)
81, 2, 3, 4, 6, 7neibastop2 35550 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ (𝑛 ∈ ((neiβ€˜π½)β€˜{𝑧}) ↔ (𝑛 βŠ† 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)))
9 velpw 4608 . . . . . . . . 9 (𝑛 ∈ 𝒫 𝑋 ↔ 𝑛 βŠ† 𝑋)
109anbi1i 623 . . . . . . . 8 ((𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…) ↔ (𝑛 βŠ† 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…))
118, 10bitr4di 288 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ (𝑛 ∈ ((neiβ€˜π½)β€˜{𝑧}) ↔ (𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)))
1211eqabdv 2866 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∣ (𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)})
13 df-rab 3432 . . . . . 6 {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…} = {𝑛 ∣ (𝑛 ∈ 𝒫 𝑋 ∧ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…)}
1412, 13eqtr4di 2789 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑋) β†’ ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
1514ralrimiva 3145 . . . 4 (πœ‘ β†’ βˆ€π‘§ ∈ 𝑋 ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
16 sneq 4639 . . . . . . 7 (π‘₯ = 𝑧 β†’ {π‘₯} = {𝑧})
1716fveq2d 6896 . . . . . 6 (π‘₯ = 𝑧 β†’ ((neiβ€˜π½)β€˜{π‘₯}) = ((neiβ€˜π½)β€˜{𝑧}))
18 fveq2 6892 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘§))
1918ineq1d 4212 . . . . . . . 8 (π‘₯ = 𝑧 β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) = ((πΉβ€˜π‘§) ∩ 𝒫 𝑛))
2019neeq1d 2999 . . . . . . 7 (π‘₯ = 𝑧 β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ… ↔ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…))
2120rabbidv 3439 . . . . . 6 (π‘₯ = 𝑧 β†’ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
2217, 21eqeq12d 2747 . . . . 5 (π‘₯ = 𝑧 β†’ (((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…}))
2322cbvralvw 3233 . . . 4 (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ βˆ€π‘§ ∈ 𝑋 ((neiβ€˜π½)β€˜{𝑧}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘§) ∩ 𝒫 𝑛) β‰  βˆ…})
2415, 23sylibr 233 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
25 toponuni 22637 . . . . . . . . . 10 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝑗)
26 eqimss2 4042 . . . . . . . . . 10 (𝑋 = βˆͺ 𝑗 β†’ βˆͺ 𝑗 βŠ† 𝑋)
2725, 26syl 17 . . . . . . . . 9 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ βˆͺ 𝑗 βŠ† 𝑋)
28 sspwuni 5104 . . . . . . . . 9 (𝑗 βŠ† 𝒫 𝑋 ↔ βˆͺ 𝑗 βŠ† 𝑋)
2927, 28sylibr 233 . . . . . . . 8 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ 𝑗 βŠ† 𝒫 𝑋)
3029ad2antlr 724 . . . . . . 7 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 βŠ† 𝒫 𝑋)
31 sseqin2 4216 . . . . . . 7 (𝑗 βŠ† 𝒫 𝑋 ↔ (𝒫 𝑋 ∩ 𝑗) = 𝑗)
3230, 31sylib 217 . . . . . 6 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ (𝒫 𝑋 ∩ 𝑗) = 𝑗)
33 topontop 22636 . . . . . . . . . . 11 (𝑗 ∈ (TopOnβ€˜π‘‹) β†’ 𝑗 ∈ Top)
3433ad3antlr 728 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ 𝑗 ∈ Top)
35 eltop2 22699 . . . . . . . . . 10 (𝑗 ∈ Top β†’ (π‘œ ∈ 𝑗 ↔ βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
3634, 35syl 17 . . . . . . . . 9 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (π‘œ ∈ 𝑗 ↔ βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
37 elpwi 4610 . . . . . . . . . . . . . . 15 (π‘œ ∈ 𝒫 𝑋 β†’ π‘œ βŠ† 𝑋)
38 ssralv 4051 . . . . . . . . . . . . . . 15 (π‘œ βŠ† 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
3937, 38syl 17 . . . . . . . . . . . . . 14 (π‘œ ∈ 𝒫 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
4039adantl 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
41 simprr 770 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
4241eleq2d 2818 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ π‘œ ∈ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
4333ad3antlr 728 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ 𝑗 ∈ Top)
4425adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) β†’ 𝑋 = βˆͺ 𝑗)
4544sseq2d 4015 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) β†’ (π‘œ βŠ† 𝑋 ↔ π‘œ βŠ† βˆͺ 𝑗))
4645biimpa 476 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ βŠ† 𝑋) β†’ π‘œ βŠ† βˆͺ 𝑗)
4737, 46sylan2 592 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ π‘œ βŠ† βˆͺ 𝑗)
4847sselda 3983 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ π‘₯ ∈ π‘œ) β†’ π‘₯ ∈ βˆͺ 𝑗)
4948adantrr 714 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ π‘₯ ∈ βˆͺ 𝑗)
5047adantr 480 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ π‘œ βŠ† βˆͺ 𝑗)
51 eqid 2731 . . . . . . . . . . . . . . . . . . 19 βˆͺ 𝑗 = βˆͺ 𝑗
5251isneip 22830 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ Top ∧ π‘₯ ∈ βˆͺ 𝑗) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ (π‘œ βŠ† βˆͺ 𝑗 ∧ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ))))
5352baibd 539 . . . . . . . . . . . . . . . . 17 (((𝑗 ∈ Top ∧ π‘₯ ∈ βˆͺ 𝑗) ∧ π‘œ βŠ† βˆͺ 𝑗) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
5443, 49, 50, 53syl21anc 835 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (π‘œ ∈ ((neiβ€˜π‘—)β€˜{π‘₯}) ↔ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ)))
55 pweq 4617 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = π‘œ β†’ 𝒫 𝑛 = 𝒫 π‘œ)
5655ineq2d 4213 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘œ β†’ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) = ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ))
5756neeq1d 2999 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘œ β†’ (((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ… ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
5857elrab3 3685 . . . . . . . . . . . . . . . . 17 (π‘œ ∈ 𝒫 𝑋 β†’ (π‘œ ∈ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
5958ad2antlr 724 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (π‘œ ∈ {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6042, 54, 593bitr3d 308 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ (π‘₯ ∈ π‘œ ∧ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})) β†’ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6160expr 456 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ π‘₯ ∈ π‘œ) β†’ (((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…)))
6261ralimdva 3166 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ π‘œ ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…)))
6340, 62syld 47 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…)))
6463imp 406 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ π‘œ ∈ 𝒫 𝑋) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6564an32s 649 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
66 ralbi 3102 . . . . . . . . . 10 (βˆ€π‘₯ ∈ π‘œ (βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…) β†’ (βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6765, 66syl 17 . . . . . . . . 9 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (βˆ€π‘₯ ∈ π‘œ βˆƒπ‘§ ∈ 𝑗 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† π‘œ) ↔ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6836, 67bitrd 278 . . . . . . . 8 ((((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ π‘œ ∈ 𝒫 𝑋) β†’ (π‘œ ∈ 𝑗 ↔ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…))
6968rabbi2dva 4218 . . . . . . 7 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ (𝒫 𝑋 ∩ 𝑗) = {π‘œ ∈ 𝒫 𝑋 ∣ βˆ€π‘₯ ∈ π‘œ ((πΉβ€˜π‘₯) ∩ 𝒫 π‘œ) β‰  βˆ…})
7069, 4eqtr4di 2789 . . . . . 6 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ (𝒫 𝑋 ∩ 𝑗) = 𝐽)
7132, 70eqtr3d 2773 . . . . 5 (((πœ‘ ∧ 𝑗 ∈ (TopOnβ€˜π‘‹)) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽)
7271expl 457 . . . 4 (πœ‘ β†’ ((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽))
7372alrimiv 1929 . . 3 (πœ‘ β†’ βˆ€π‘—((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽))
74 eleq1 2820 . . . . 5 (𝑗 = 𝐽 β†’ (𝑗 ∈ (TopOnβ€˜π‘‹) ↔ 𝐽 ∈ (TopOnβ€˜π‘‹)))
75 fveq2 6892 . . . . . . . 8 (𝑗 = 𝐽 β†’ (neiβ€˜π‘—) = (neiβ€˜π½))
7675fveq1d 6894 . . . . . . 7 (𝑗 = 𝐽 β†’ ((neiβ€˜π‘—)β€˜{π‘₯}) = ((neiβ€˜π½)β€˜{π‘₯}))
7776eqeq1d 2733 . . . . . 6 (𝑗 = 𝐽 β†’ (((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
7877ralbidv 3176 . . . . 5 (𝑗 = 𝐽 β†’ (βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
7974, 78anbi12d 630 . . . 4 (𝑗 = 𝐽 β†’ ((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ↔ (𝐽 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})))
8079eqeu 3703 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (𝐽 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π½)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) ∧ βˆ€π‘—((𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}) β†’ 𝑗 = 𝐽)) β†’ βˆƒ!𝑗(𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
815, 5, 24, 73, 80syl121anc 1374 . 2 (πœ‘ β†’ βˆƒ!𝑗(𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
82 df-reu 3376 . 2 (βˆƒ!𝑗 ∈ (TopOnβ€˜π‘‹)βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…} ↔ βˆƒ!𝑗(𝑗 ∈ (TopOnβ€˜π‘‹) ∧ βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…}))
8381, 82sylibr 233 1 (πœ‘ β†’ βˆƒ!𝑗 ∈ (TopOnβ€˜π‘‹)βˆ€π‘₯ ∈ 𝑋 ((neiβ€˜π‘—)β€˜{π‘₯}) = {𝑛 ∈ 𝒫 𝑋 ∣ ((πΉβ€˜π‘₯) ∩ 𝒫 𝑛) β‰  βˆ…})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086  βˆ€wal 1538   = wceq 1540   ∈ wcel 2105  βˆƒ!weu 2561  {cab 2708   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  βˆƒ!wreu 3373  {crab 3431   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βŸΆwf 6540  β€˜cfv 6544  Topctop 22616  TopOnctopon 22633  neicnei 22822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7415  df-om 7859  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-topgen 17394  df-top 22617  df-topon 22634  df-nei 22823
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator