Theorem oldlim

Description: The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	oldlim	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to \mathrm{Old}\left(A\right)=\bigcup \mathrm{Old}\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		simprl	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> c e. A ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> c e. A ) with typecode |-
2		limsuc	$$⊢\mathrm{Lim}A\to \left(c\in A\leftrightarrow \mathrm{suc}c\in A\right)$$
3	2	ad2antrr	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> ( c e. A <-> suc c e. A ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> ( c e. A <-> suc c e. A ) ) with typecode |-
4	1 3	mpbid	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> suc c e. A ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> suc c e. A ) with typecode |-
5		simprr	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> x e. ( _Made ` c ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> x e. ( _Made ` c ) ) with typecode |-
6		limord	$$⊢\mathrm{Lim}A\to \mathrm{Ord}A$$
7		elex	$$⊢A\in V\to A\in \mathrm{V}$$
8	6 7	anim12i	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to \left(\mathrm{Ord}A\wedge A\in \mathrm{V}\right)$$
9		elon2	$$⊢A\in \mathrm{On}\leftrightarrow \left(\mathrm{Ord}A\wedge A\in \mathrm{V}\right)$$
10	8 9	sylibr	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to A\in \mathrm{On}$$
11		onelon	$$⊢\left(A\in \mathrm{On}\wedge c\in A\right)\to c\in \mathrm{On}$$
12	10 1 11	syl2an2r	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> c e. On ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> c e. On ) with typecode |-
13		madeoldsuc	Could not format ( c e. On -> ( _Made ` c ) = ( _Old ` suc c ) ) : No typesetting found for |- ( c e. On -> ( _Made ` c ) = ( _Old ` suc c ) ) with typecode |-
14	12 13	syl	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> ( _Made ` c ) = ( _Old ` suc c ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> ( _Made ` c ) = ( _Old ` suc c ) ) with typecode |-
15	5 14	eleqtrd	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> x e. ( _Old ` suc c ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> x e. ( _Old ` suc c ) ) with typecode |-
16		fveq2	$$⊢b=\mathrm{suc}c\to \mathrm{Old}\left(b\right)=\mathrm{Old}\left(\mathrm{suc}c\right)$$
17	16	eleq2d	$$⊢b=\mathrm{suc}c\to \left(x\in \mathrm{Old}\left(b\right)\leftrightarrow x\in \mathrm{Old}\left(\mathrm{suc}c\right)\right)$$
18	17	rspcev	$$⊢\left(\mathrm{suc}c\in A\wedge x\in \mathrm{Old}\left(\mathrm{suc}c\right)\right)\to \exists b\in Ax\in \mathrm{Old}\left(b\right)$$
19	4 15 18	syl2anc	Could not format ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> E. b e. A x e. ( _Old ` b ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( c e. A /\ x e. ( _Made ` c ) ) ) -> E. b e. A x e. ( _Old ` b ) ) with typecode |-
20	19	rexlimdvaa	Could not format ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _Made ` c ) -> E. b e. A x e. ( _Old ` b ) ) ) : No typesetting found for |- ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _Made ` c ) -> E. b e. A x e. ( _Old ` b ) ) ) with typecode |-
21		simprl	$$⊢\left(\left(\mathrm{Lim}A\wedge A\in V\right)\wedge \left(b\in A\wedge x\in \mathrm{Old}\left(b\right)\right)\right)\to b\in A$$
22		oldssmade	Could not format ( _Old ` b ) C_ ( _Made ` b ) : No typesetting found for |- ( _Old ` b ) C_ ( _Made ` b ) with typecode |-
23		simprr	$$⊢\left(\left(\mathrm{Lim}A\wedge A\in V\right)\wedge \left(b\in A\wedge x\in \mathrm{Old}\left(b\right)\right)\right)\to x\in \mathrm{Old}\left(b\right)$$
24	22 23	sselid	Could not format ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> x e. ( _Made ` b ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> x e. ( _Made ` b ) ) with typecode |-
25		fveq2	Could not format ( c = b -> ( _Made ` c ) = ( _Made ` b ) ) : No typesetting found for |- ( c = b -> ( _Made ` c ) = ( _Made ` b ) ) with typecode |-
26	25	eleq2d	Could not format ( c = b -> ( x e. ( _Made ` c ) <-> x e. ( _Made ` b ) ) ) : No typesetting found for |- ( c = b -> ( x e. ( _Made ` c ) <-> x e. ( _Made ` b ) ) ) with typecode |-
27	26	rspcev	Could not format ( ( b e. A /\ x e. ( _Made ` b ) ) -> E. c e. A x e. ( _Made ` c ) ) : No typesetting found for |- ( ( b e. A /\ x e. ( _Made ` b ) ) -> E. c e. A x e. ( _Made ` c ) ) with typecode |-
28	21 24 27	syl2anc	Could not format ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> E. c e. A x e. ( _Made ` c ) ) : No typesetting found for |- ( ( ( Lim A /\ A e. V ) /\ ( b e. A /\ x e. ( _Old ` b ) ) ) -> E. c e. A x e. ( _Made ` c ) ) with typecode |-
29	28	rexlimdvaa	Could not format ( ( Lim A /\ A e. V ) -> ( E. b e. A x e. ( _Old ` b ) -> E. c e. A x e. ( _Made ` c ) ) ) : No typesetting found for |- ( ( Lim A /\ A e. V ) -> ( E. b e. A x e. ( _Old ` b ) -> E. c e. A x e. ( _Made ` c ) ) ) with typecode |-
30	20 29	impbid	Could not format ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _Made ` c ) <-> E. b e. A x e. ( _Old ` b ) ) ) : No typesetting found for |- ( ( Lim A /\ A e. V ) -> ( E. c e. A x e. ( _Made ` c ) <-> E. b e. A x e. ( _Old ` b ) ) ) with typecode |-
31		elold	Could not format ( A e. On -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _Made ` c ) ) ) : No typesetting found for |- ( A e. On -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _Made ` c ) ) ) with typecode |-
32	10 31	syl	Could not format ( ( Lim A /\ A e. V ) -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _Made ` c ) ) ) : No typesetting found for |- ( ( Lim A /\ A e. V ) -> ( x e. ( _Old ` A ) <-> E. c e. A x e. ( _Made ` c ) ) ) with typecode |-
33		eliun	$$⊢x\in \bigcup _{b\in A}\mathrm{Old}\left(b\right)\leftrightarrow \exists b\in Ax\in \mathrm{Old}\left(b\right)$$
34	33	a1i	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to \left(x\in \bigcup _{b\in A}\mathrm{Old}\left(b\right)\leftrightarrow \exists b\in Ax\in \mathrm{Old}\left(b\right)\right)$$
35	30 32 34	3bitr4d	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to \left(x\in \mathrm{Old}\left(A\right)\leftrightarrow x\in \bigcup _{b\in A}\mathrm{Old}\left(b\right)\right)$$
36	35	eqrdv	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to \mathrm{Old}\left(A\right)=\bigcup _{b\in A}\mathrm{Old}\left(b\right)$$
37		oldf	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$
38		ffun	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}\to \mathrm{Fun}\mathrm{Old}$$
39		funiunfv	$$⊢\mathrm{Fun}\mathrm{Old}\to \bigcup _{b\in A}\mathrm{Old}\left(b\right)=\bigcup \mathrm{Old}\left[A\right]$$
40	37 38 39	mp2b	$$⊢\bigcup _{b\in A}\mathrm{Old}\left(b\right)=\bigcup \mathrm{Old}\left[A\right]$$
41	36 40	eqtrdi	$$⊢\left(\mathrm{Lim}A\wedge A\in V\right)\to \mathrm{Old}\left(A\right)=\bigcup \mathrm{Old}\left[A\right]$$