Metamath Proof Explorer

Theorem onsuplub

Description: The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025)

Ref Expression
Assertion onsuplub ⊢ A ⊆ On ∧ A ∈ V ∧ B ∈ On → B ∈ ⋃ A ↔ ∃ z ∈ A B ∈ z

Proof

Step Hyp Ref Expression
1 eluni2 ⊢ B ∈ ⋃ A ↔ ∃ z ∈ A B ∈ z
2 1 a1i ⊢ A ⊆ On ∧ A ∈ V ∧ B ∈ On → B ∈ ⋃ A ↔ ∃ z ∈ A B ∈ z