Theorem oninfex2

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

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

Proof

Step	Hyp	Ref	Expression
1		onintunirab	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } )
2		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
3	2	biimpi	⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ∈ V )
4	3	adantl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ V )
5	1 4	eqeltrrd	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∪ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 } ∈ V )