Theorem oldlim

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

	Ref	Expression
Assertion	oldlim	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( O ‘ 𝐴 ) = ∪ ( O “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑐 ∈ 𝐴 )
2		limsuc	⊢ ( Lim 𝐴 → ( 𝑐 ∈ 𝐴 ↔ suc 𝑐 ∈ 𝐴 ) )
3	2	ad2antrr	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → ( 𝑐 ∈ 𝐴 ↔ suc 𝑐 ∈ 𝐴 ) )
4	1 3	mpbid	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → suc 𝑐 ∈ 𝐴 )
5		simprr	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑥 ∈ ( M ‘ 𝑐 ) )
6		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
7		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
8	6 7	anim12i	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( Ord 𝐴 ∧ 𝐴 ∈ V ) )
9		elon2	⊢ ( 𝐴 ∈ On ↔ ( Ord 𝐴 ∧ 𝐴 ∈ V ) )
10	8 9	sylibr	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ On )
11		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ On )
12	10 1 11	syl2an2r	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑐 ∈ On )
13		madeoldsuc	⊢ ( 𝑐 ∈ On → ( M ‘ 𝑐 ) = ( O ‘ suc 𝑐 ) )
14	12 13	syl	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → ( M ‘ 𝑐 ) = ( O ‘ suc 𝑐 ) )
15	5 14	eleqtrd	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → 𝑥 ∈ ( O ‘ suc 𝑐 ) )
16		fveq2	⊢ ( 𝑏 = suc 𝑐 → ( O ‘ 𝑏 ) = ( O ‘ suc 𝑐 ) )
17	16	eleq2d	⊢ ( 𝑏 = suc 𝑐 → ( 𝑥 ∈ ( O ‘ 𝑏 ) ↔ 𝑥 ∈ ( O ‘ suc 𝑐 ) ) )
18	17	rspcev	⊢ ( ( suc 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ suc 𝑐 ) ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) )
19	4 15 18	syl2anc	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑐 ) ) ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) )
20	19	rexlimdvaa	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) → ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) )
21		simprl	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑏 ∈ 𝐴 )
22		oldssmade	⊢ ( O ‘ 𝑏 ) ⊆ ( M ‘ 𝑏 )
23		simprr	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑥 ∈ ( O ‘ 𝑏 ) )
24	22 23	sselid	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → 𝑥 ∈ ( M ‘ 𝑏 ) )
25		fveq2	⊢ ( 𝑐 = 𝑏 → ( M ‘ 𝑐 ) = ( M ‘ 𝑏 ) )
26	25	eleq2d	⊢ ( 𝑐 = 𝑏 → ( 𝑥 ∈ ( M ‘ 𝑐 ) ↔ 𝑥 ∈ ( M ‘ 𝑏 ) ) )
27	26	rspcev	⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( M ‘ 𝑏 ) ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) )
28	21 24 27	syl2anc	⊢ ( ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑥 ∈ ( O ‘ 𝑏 ) ) ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) )
29	28	rexlimdvaa	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) → ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) )
30	20 29	impbid	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) )
31		elold	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) )
32	10 31	syl	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ( M ‘ 𝑐 ) ) )
33		eliun	⊢ ( 𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) )
34	33	a1i	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑥 ∈ ( O ‘ 𝑏 ) ) )
35	30 32 34	3bitr4d	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( O ‘ 𝐴 ) ↔ 𝑥 ∈ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) ) )
36	35	eqrdv	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( O ‘ 𝐴 ) = ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) )
37		oldf	⊢ O : On ⟶ 𝒫 No
38		ffun	⊢ ( O : On ⟶ 𝒫 No → Fun O )
39		funiunfv	⊢ ( Fun O → ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) = ∪ ( O “ 𝐴 ) )
40	37 38 39	mp2b	⊢ ∪ 𝑏 ∈ 𝐴 ( O ‘ 𝑏 ) = ∪ ( O “ 𝐴 )
41	36 40	eqtrdi	⊢ ( ( Lim 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( O ‘ 𝐴 ) = ∪ ( O “ 𝐴 ) )