Metamath Proof Explorer

Theorem onsupuni2

Description: The supremum of a set of ordinals is the union of that set. (Contributed by RP, 22-Jan-2025)

		Ref	Expression
	Assertion	onsupuni2	$⊢ A \in 𝒫 On \to sup (A, On, E) = ⋃ A$

Step	Hyp	Ref	Expression
1		elpwb	$⊢ A \in 𝒫 On \leftrightarrow (A \in V \land A \subseteq On)$
2		onsupuni	$⊢ (A \subseteq On \land A \in V) \to sup (A, On, E) = ⋃ A$
3	2	ancoms	$⊢ (A \in V \land A \subseteq On) \to sup (A, On, E) = ⋃ A$
4	1 3	sylbi	$⊢ A \in 𝒫 On \to sup (A, On, E) = ⋃ A$