This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inton

Description: The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003)

		Ref	Expression
	Assertion	inton	$⊢ ⋂ On = \emptyset$

Step	Hyp	Ref	Expression
1		0elon	$⊢ \emptyset \in On$
2		int0el	$⊢ \emptyset \in On \to ⋂ On = \emptyset$
3	1 2	ax-mp	$⊢ ⋂ On = \emptyset$