istps

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

	Ref	Expression
Hypotheses	istps.a	$⊢ A = {Base}_{K}$
	istps.j	$⊢ J = TopOpen (K)$
Assertion	istps	$⊢ K \in TopSp \leftrightarrow J \in TopOn (A)$

Step	Hyp	Ref	Expression
1		istps.a	$⊢ A = {Base}_{K}$
2		istps.j	$⊢ J = TopOpen (K)$
3		df-topsp	$⊢ TopSp = \{f \| TopOpen (f) \in TopOn ({Base}_{f})\}$
4	3	eleq2i	$⊢ K \in TopSp \leftrightarrow K \in \{f \| TopOpen (f) \in TopOn ({Base}_{f})\}$
5		topontop	$⊢ J \in TopOn (A) \to J \in Top$
6		0ntop	$⊢ \neg \emptyset \in Top$
7		fvprc	$⊢ \neg K \in V \to TopOpen (K) = \emptyset$
8	2 7	eqtrid	$⊢ \neg K \in V \to J = \emptyset$
9	8	eleq1d	$⊢ \neg K \in V \to (J \in Top \leftrightarrow \emptyset \in Top)$
10	6 9	mtbiri	$⊢ \neg K \in V \to \neg J \in Top$
11	10	con4i	$⊢ J \in Top \to K \in V$
12	5 11	syl	$⊢ J \in TopOn (A) \to K \in V$
13		fveq2	$⊢ f = K \to TopOpen (f) = TopOpen (K)$
14	13 2	eqtr4di	$⊢ f = K \to TopOpen (f) = J$
15		fveq2	$⊢ f = K \to {Base}_{f} = {Base}_{K}$
16	15 1	eqtr4di	$⊢ f = K \to {Base}_{f} = A$
17	16	fveq2d	$⊢ f = K \to TopOn ({Base}_{f}) = TopOn (A)$
18	14 17	eleq12d	$⊢ f = K \to (TopOpen (f) \in TopOn ({Base}_{f}) \leftrightarrow J \in TopOn (A))$
19	12 18	elab3	$⊢ K \in \{f \| TopOpen (f) \in TopOn ({Base}_{f})\} \leftrightarrow J \in TopOn (A)$
20	4 19	bitri	$⊢ K \in TopSp \leftrightarrow J \in TopOn (A)$

Metamath Proof Explorer