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

Metamath Proof Explorer

Theorem ordin

Description: The intersection of two ordinal classes is ordinal. Proposition 7.9 of TakeutiZaring p. 37. (Contributed by NM, 9-May-1994)

		Ref	Expression
	Assertion	ordin	$⊢ (Ord A \land Ord B) \to Ord (A \cap B)$

Step	Hyp	Ref	Expression
1		ordtr	$⊢ Ord A \to Tr A$
2		ordtr	$⊢ Ord B \to Tr B$
3		trin	$⊢ (Tr A \land Tr B) \to Tr (A \cap B)$
4	1 2 3	syl2an	$⊢ (Ord A \land Ord B) \to Tr (A \cap B)$
5		inss2	$⊢ A \cap B \subseteq B$
6		trssord	$⊢ (Tr (A \cap B) \land A \cap B \subseteq B \land Ord B) \to Ord (A \cap B)$
7	5 6	mp3an2	$⊢ (Tr (A \cap B) \land Ord B) \to Ord (A \cap B)$
8	4 7	sylancom	$⊢ (Ord A \land Ord B) \to Ord (A \cap B)$