Theorem limexissup

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

	Ref	Expression
Assertion	limexissup	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to A=sup\left(A,\mathrm{On},\mathrm{E}\right)$$

Proof

Step	Hyp	Ref	Expression
1		limuni	$$⊢\mathrm{Lim}A\to A=\bigcup A$$
2	1	adantr	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to A=\bigcup A$$
3		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
4		ordsson	$$⊢\mathrm{Ord}A\to A\subseteq \mathrm{On}$$
5	3 4	syl	$$⊢\mathrm{Lim}A\to A\subseteq \mathrm{On}$$
6		onsupuni	$$⊢\left(A\subseteq \mathrm{On}\wedge A\in V\right)\to sup\left(A,\mathrm{On},\mathrm{E}\right)=\bigcup A$$
7	5 6	sylan	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to sup\left(A,\mathrm{On},\mathrm{E}\right)=\bigcup A$$
8	2 7	eqtr4d	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to A=sup\left(A,\mathrm{On},\mathrm{E}\right)$$