Theorem onin

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

	Ref	Expression
Assertion	onin	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∩ 𝐵 ) ∈ On )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
3		ordin	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord ( 𝐴 ∩ 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord ( 𝐴 ∩ 𝐵 ) )
5		simpl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
6		inex1g	⊢ ( 𝐴 ∈ On → ( 𝐴 ∩ 𝐵 ) ∈ V )
7		elong	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ V → ( ( 𝐴 ∩ 𝐵 ) ∈ On ↔ Ord ( 𝐴 ∩ 𝐵 ) ) )
8	5 6 7	3syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∩ 𝐵 ) ∈ On ↔ Ord ( 𝐴 ∩ 𝐵 ) ) )
9	4 8	mpbird	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∩ 𝐵 ) ∈ On )