oldlim

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

		Ref	Expression
	Assertion	oldlim	$⊢ (Lim A \land A \in V) \to Old (A) = ⋃ Old [A]$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to c \in A$
2		limsuc	$⊢ Lim A \to (c \in A \leftrightarrow suc c \in A)$
3	2	ad2antrr	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to (c \in A \leftrightarrow suc c \in A)$
4	1 3	mpbid	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to suc c \in A$
5		simprr	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to x \in M (c)$
6		limord	$⊢ Lim A \to Ord A$
7		elex	$⊢ A \in V \to A \in V$
8	6 7	anim12i	$⊢ (Lim A \land A \in V) \to (Ord A \land A \in V)$
9		elon2	$⊢ A \in On \leftrightarrow (Ord A \land A \in V)$
10	8 9	sylibr	$⊢ (Lim A \land A \in V) \to A \in On$
11		onelon	$⊢ (A \in On \land c \in A) \to c \in On$
12	10 1 11	syl2an2r	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to c \in On$
13		madeoldsuc	$⊢ c \in On \to M (c) = Old (suc c)$
14	12 13	syl	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to M (c) = Old (suc c)$
15	5 14	eleqtrd	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to x \in Old (suc c)$
16		fveq2	$⊢ b = suc c \to Old (b) = Old (suc c)$
17	16	eleq2d	$⊢ b = suc c \to (x \in Old (b) \leftrightarrow x \in Old (suc c))$
18	17	rspcev	$⊢ (suc c \in A \land x \in Old (suc c)) \to \exists b \in A x \in Old (b)$
19	4 15 18	syl2anc	$⊢ ((Lim A \land A \in V) \land (c \in A \land x \in M (c))) \to \exists b \in A x \in Old (b)$
20	19	expr	$⊢ ((Lim A \land A \in V) \land c \in A) \to (x \in M (c) \to \exists b \in A x \in Old (b))$
21	20	rexlimdva	$⊢ (Lim A \land A \in V) \to (\exists c \in A x \in M (c) \to \exists b \in A x \in Old (b))$
22		simprl	$⊢ ((Lim A \land A \in V) \land (b \in A \land x \in Old (b))) \to b \in A$
23		onelon	$⊢ (A \in On \land b \in A) \to b \in On$
24	10 22 23	syl2an2r	$⊢ ((Lim A \land A \in V) \land (b \in A \land x \in Old (b))) \to b \in On$
25		oldssmade	$⊢ b \in On \to Old (b) \subseteq M (b)$
26	24 25	syl	$⊢ ((Lim A \land A \in V) \land (b \in A \land x \in Old (b))) \to Old (b) \subseteq M (b)$
27		simprr	$⊢ ((Lim A \land A \in V) \land (b \in A \land x \in Old (b))) \to x \in Old (b)$
28	26 27	sseldd	$⊢ ((Lim A \land A \in V) \land (b \in A \land x \in Old (b))) \to x \in M (b)$
29		fveq2	$⊢ c = b \to M (c) = M (b)$
30	29	eleq2d	$⊢ c = b \to (x \in M (c) \leftrightarrow x \in M (b))$
31	30	rspcev	$⊢ (b \in A \land x \in M (b)) \to \exists c \in A x \in M (c)$
32	22 28 31	syl2anc	$⊢ ((Lim A \land A \in V) \land (b \in A \land x \in Old (b))) \to \exists c \in A x \in M (c)$
33	32	expr	$⊢ ((Lim A \land A \in V) \land b \in A) \to (x \in Old (b) \to \exists c \in A x \in M (c))$
34	33	rexlimdva	$⊢ (Lim A \land A \in V) \to (\exists b \in A x \in Old (b) \to \exists c \in A x \in M (c))$
35	21 34	impbid	$⊢ (Lim A \land A \in V) \to (\exists c \in A x \in M (c) \leftrightarrow \exists b \in A x \in Old (b))$
36		elold	$⊢ A \in On \to (x \in Old (A) \leftrightarrow \exists c \in A x \in M (c))$
37	10 36	syl	$⊢ (Lim A \land A \in V) \to (x \in Old (A) \leftrightarrow \exists c \in A x \in M (c))$
38		eliun	$⊢ x \in ⋃_{b \in A} Old (b) \leftrightarrow \exists b \in A x \in Old (b)$
39	38	a1i	$⊢ (Lim A \land A \in V) \to (x \in ⋃_{b \in A} Old (b) \leftrightarrow \exists b \in A x \in Old (b))$
40	35 37 39	3bitr4d	$⊢ (Lim A \land A \in V) \to (x \in Old (A) \leftrightarrow x \in ⋃_{b \in A} Old (b))$
41	40	eqrdv	$⊢ (Lim A \land A \in V) \to Old (A) = ⋃_{b \in A} Old (b)$
42		oldf	$⊢ Old : On ⟶ 𝒫 No$
43		ffun	$⊢ Old : On ⟶ 𝒫 No \to Fun Old$
44		funiunfv	$⊢ Fun Old \to ⋃_{b \in A} Old (b) = ⋃ Old [A]$
45	42 43 44	mp2b	$⊢ ⋃_{b \in A} Old (b) = ⋃ Old [A]$
46	41 45	eqtrdi	$⊢ (Lim A \land A \in V) \to Old (A) = ⋃ Old [A]$

Metamath Proof Explorer

Theorem oldlim

Proof