This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istps

Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypotheses istps.a ⊢ 𝐴 = ( Base ‘ 𝐾 )
istps.j ⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
Assertion istps ( 𝐾 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 istps.a ⊢ 𝐴 = ( Base ‘ 𝐾 )
2 istps.j ⊢ 𝐽 = ( TopOpen ‘ 𝐾 )
3 df-topsp ⊢ TopSp = { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) }
4 3 eleq2i ⊢ ( 𝐾 ∈ TopSp ↔ 𝐾 ∈ { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) } )
5 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐽 ∈ Top )
6 0ntop ⊢ ¬ ∅ ∈ Top
7 fvprc ⊢ ( ¬ 𝐾 ∈ V → ( TopOpen ‘ 𝐾 ) = ∅ )
8 2 7 eqtrid ⊢ ( ¬ 𝐾 ∈ V → 𝐽 = ∅ )
9 8 eleq1d ⊢ ( ¬ 𝐾 ∈ V → ( 𝐽 ∈ Top ↔ ∅ ∈ Top ) )
10 6 9 mtbiri ⊢ ( ¬ 𝐾 ∈ V → ¬ 𝐽 ∈ Top )
11 10 con4i ⊢ ( 𝐽 ∈ Top → 𝐾 ∈ V )
12 5 11 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ V )
13 fveq2 ⊢ ( 𝑓 = 𝐾 → ( TopOpen ‘ 𝑓 ) = ( TopOpen ‘ 𝐾 ) )
14 13 2 eqtr4di ⊢ ( 𝑓 = 𝐾 → ( TopOpen ‘ 𝑓 ) = 𝐽 )
15 fveq2 ⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) )
16 15 1 eqtr4di ⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = 𝐴 )
17 16 fveq2d ⊢ ( 𝑓 = 𝐾 → ( TopOn ‘ ( Base ‘ 𝑓 ) ) = ( TopOn ‘ 𝐴 ) )
18 14 17 eleq12d ⊢ ( 𝑓 = 𝐾 → ( ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) ) )
19 12 18 elab3 ⊢ ( 𝐾 ∈ { 𝑓 ∣ ( TopOpen ‘ 𝑓 ) ∈ ( TopOn ‘ ( Base ‘ 𝑓 ) ) } ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) )
20 4 19 bitri ⊢ ( 𝐾 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐴 ) )