Theorem istopg

Description: Express the predicate " J is a topology". See istop2g for another characterization using nonempty finite intersections instead of binary intersections.

Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Assertion	istopg	$$⊢J\in A\to \left(J\in \mathrm{Top}\leftrightarrow \left(\forall x\left(x\subseteq J\to \bigcup x\in J\right)\wedge \forall x\in J\forall y\in Jx\cap y\in J\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pweq	$$⊢z=J\to 𝒫z=𝒫J$$
2		eleq2	$$⊢z=J\to \left(\bigcup x\in z\leftrightarrow \bigcup x\in J\right)$$
3	1 2	raleqbidv	$$⊢z=J\to \left(\forall x\in 𝒫z\bigcup x\in z\leftrightarrow \forall x\in 𝒫J\bigcup x\in J\right)$$
4		eleq2	$$⊢z=J\to \left(x\cap y\in z\leftrightarrow x\cap y\in J\right)$$
5	4	raleqbi1dv	$$⊢z=J\to \left(\forall y\in zx\cap y\in z\leftrightarrow \forall y\in Jx\cap y\in J\right)$$
6	5	raleqbi1dv	$$⊢z=J\to \left(\forall x\in z\forall y\in zx\cap y\in z\leftrightarrow \forall x\in J\forall y\in Jx\cap y\in J\right)$$
7	3 6	anbi12d	$$⊢z=J\to \left(\left(\forall x\in 𝒫z\bigcup x\in z\wedge \forall x\in z\forall y\in zx\cap y\in z\right)\leftrightarrow \left(\forall x\in 𝒫J\bigcup x\in J\wedge \forall x\in J\forall y\in Jx\cap y\in J\right)\right)$$
8		df-top	$$⊢\mathrm{Top}=\left\{z|\left(\forall x\in 𝒫z\bigcup x\in z\wedge \forall x\in z\forall y\in zx\cap y\in z\right)\right\}$$
9	7 8	elab2g	$$⊢J\in A\to \left(J\in \mathrm{Top}\leftrightarrow \left(\forall x\in 𝒫J\bigcup x\in J\wedge \forall x\in J\forall y\in Jx\cap y\in J\right)\right)$$
10		df-ral	$$⊢\forall x\in 𝒫J\bigcup x\in J\leftrightarrow \forall x\left(x\in 𝒫J\to \bigcup x\in J\right)$$
11		elpw2g	$$⊢J\in A\to \left(x\in 𝒫J\leftrightarrow x\subseteq J\right)$$
12	11	imbi1d	$$⊢J\in A\to \left(\left(x\in 𝒫J\to \bigcup x\in J\right)\leftrightarrow \left(x\subseteq J\to \bigcup x\in J\right)\right)$$
13	12	albidv	$$⊢J\in A\to \left(\forall x\left(x\in 𝒫J\to \bigcup x\in J\right)\leftrightarrow \forall x\left(x\subseteq J\to \bigcup x\in J\right)\right)$$
14	10 13	bitrid	$$⊢J\in A\to \left(\forall x\in 𝒫J\bigcup x\in J\leftrightarrow \forall x\left(x\subseteq J\to \bigcup x\in J\right)\right)$$
15	14	anbi1d	$$⊢J\in A\to \left(\left(\forall x\in 𝒫J\bigcup x\in J\wedge \forall x\in J\forall y\in Jx\cap y\in J\right)\leftrightarrow \left(\forall x\left(x\subseteq J\to \bigcup x\in J\right)\wedge \forall x\in J\forall y\in Jx\cap y\in J\right)\right)$$
16	9 15	bitrd	$$⊢J\in A\to \left(J\in \mathrm{Top}\leftrightarrow \left(\forall x\left(x\subseteq J\to \bigcup x\in J\right)\wedge \forall x\in J\forall y\in Jx\cap y\in J\right)\right)$$