onin

Description: The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995)

		Ref	Expression
	Assertion	onin	$⊢ (A \in On \land B \in On) \to A \cap B \in On$

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		eloni	$⊢ B \in On \to Ord B$
3		ordin	$⊢ (Ord A \land Ord B) \to Ord (A \cap B)$
4	1 2 3	syl2an	$⊢ (A \in On \land B \in On) \to Ord (A \cap B)$
5		simpl	$⊢ (A \in On \land B \in On) \to A \in On$
6		inex1g	$⊢ A \in On \to A \cap B \in V$
7		elong	$⊢ A \cap B \in V \to (A \cap B \in On \leftrightarrow Ord (A \cap B))$
8	5 6 7	3syl	$⊢ (A \in On \land B \in On) \to (A \cap B \in On \leftrightarrow Ord (A \cap B))$
9	4 8	mpbird	$⊢ (A \in On \land B \in On) \to A \cap B \in On$

Metamath Proof Explorer