Metamath Proof Explorer

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 ⁡ A ∧ A ∈ V → Old ⁡ A = ⋃ Old A

Proof

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