Metamath Proof Explorer

Theorem onsupintrab2

Description: The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025)

		Ref	Expression
	Assertion	onsupintrab2	$⊢ A \in 𝒫 On \to sup (A, On, E) = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$

Proof

Step	Hyp	Ref	Expression
1		elpwb	$⊢ A \in 𝒫 On \leftrightarrow (A \in V \land A \subseteq On)$
2		onsupintrab	$⊢ (A \subseteq On \land A \in V) \to sup (A, On, E) = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$
3	2	ancoms	$⊢ (A \in V \land A \subseteq On) \to sup (A, On, E) = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$
4	1 3	sylbi	$⊢ A \in 𝒫 On \to sup (A, On, E) = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$