Metamath Proof Explorer

Theorem limexissupab

Description: An ordinal which is a limit ordinal is equal to the supremum of the class of all its elements. Lemma 2.13 of Schloeder p. 5. (Contributed by RP, 27-Jan-2025)

		Ref	Expression
	Assertion	limexissupab	$⊢ (Lim A \land A \in V) \to A = sup (\{x \| x \in A\}, On, E)$

Proof

Step	Hyp	Ref	Expression
1		limuni	$⊢ Lim A \to A = ⋃ A$
2	1	adantr	$⊢ (Lim A \land A \in V) \to A = ⋃ A$
3		limord	$⊢ Lim A \to Ord A$
4		ordsson	$⊢ Ord A \to A \subseteq On$
5	3 4	syl	$⊢ Lim A \to A \subseteq On$
6		onsupuni	$⊢ (A \subseteq On \land A \in V) \to sup (A, On, E) = ⋃ A$
7	5 6	sylan	$⊢ (Lim A \land A \in V) \to sup (A, On, E) = ⋃ A$
8		abid1	$⊢ A = \{x \| x \in A\}$
9		supeq1	$⊢ A = \{x \| x \in A\} \to sup (A, On, E) = sup (\{x \| x \in A\}, On, E)$
10	8 9	mp1i	$⊢ (Lim A \land A \in V) \to sup (A, On, E) = sup (\{x \| x \in A\}, On, E)$
11	2 7 10	3eqtr2d	$⊢ (Lim A \land A \in V) \to A = sup (\{x \| x \in A\}, On, E)$