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 syl5eq ( ¬ 𝐾 ∈ 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 ‘ 𝐴 ) )