Metamath Proof Explorer

Theorem istop2g

Description: Express the predicate " J is a topology" using nonempty finite intersections instead of binary intersections as in istopg . (Contributed by NM, 19-Jul-2006)

		Ref	Expression
	Assertion	istop2g	$⊢ J \in A \to (J \in Top \leftrightarrow (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x ((x \subseteq J \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in J)))$

Proof

Step	Hyp	Ref	Expression
1		istopg	$⊢ J \in A \to (J \in Top \leftrightarrow (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x \in J \forall y \in J x \cap y \in J))$
2		fiint	$⊢ \forall x \in J \forall y \in J x \cap y \in J \leftrightarrow \forall x ((x \subseteq J \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in J)$
3	2	anbi2i	$⊢ (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x \in J \forall y \in J x \cap y \in J) \leftrightarrow (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x ((x \subseteq J \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in J))$
4	1 3	bitrdi	$⊢ J \in A \to (J \in Top \leftrightarrow (\forall x (x \subseteq J \to ⋃ x \in J) \land \forall x ((x \subseteq J \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in J)))$