Theorem oninfcl2

Description: The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfcl2	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ On )

Proof

Step	Hyp	Ref	Expression
1		onintunirab	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )
2		oninton	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )
3	1 2	eqeltrrd	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ On )