Theorem oninfunirab

Description: The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025)

	Ref	Expression
Assertion	oninfunirab	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , On , E ) = ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )

Proof

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