Theorem oninton

Description: The intersection of a nonempty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of TakeutiZaring p. 44. (Contributed by NM, 29-Jan-1997)

	Ref	Expression
Assertion	oninton	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		onint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )
2	1	ex	⊢ ( 𝐴 ⊆ On → ( 𝐴 ≠ ∅ → ∩ 𝐴 ∈ 𝐴 ) )
3		ssel	⊢ ( 𝐴 ⊆ On → ( ∩ 𝐴 ∈ 𝐴 → ∩ 𝐴 ∈ On ) )
4	2 3	syld	⊢ ( 𝐴 ⊆ On → ( 𝐴 ≠ ∅ → ∩ 𝐴 ∈ On ) )
5	4	imp	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )