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 ‘ 𝐴 ) )