onintopssconn

Description: An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015)

		Ref	Expression
	Assertion	onintopssconn	$⊢ On \cap Top \subseteq Conn$

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (On \cap Top) \leftrightarrow (x \in On \land x \in Top)$
2		eloni	$⊢ x \in On \to Ord x$
3		ordtopconn	$⊢ Ord x \to (x \in Top \leftrightarrow x \in Conn)$
4	2 3	syl	$⊢ x \in On \to (x \in Top \leftrightarrow x \in Conn)$
5	4	biimpa	$⊢ (x \in On \land x \in Top) \to x \in Conn$
6	1 5	sylbi	$⊢ x \in (On \cap Top) \to x \in Conn$
7	6	ssriv	$⊢ On \cap Top \subseteq Conn$

Metamath Proof Explorer