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 simprr ⊢ Lim ⁡ A ∧ A ∈ V ∧ b ∈ A ∧ x ∈ Old ⁡ b → x ∈ Old ⁡ b
23 22 oldmaded ⊢ Lim ⁡ A ∧ A ∈ V ∧ b ∈ A ∧ x ∈ Old ⁡ b → x ∈ M ⁡ b
24 fveq2 ⊢ c = b → M ⁡ c = M ⁡ b
25 24 eleq2d ⊢ c = b → x ∈ M ⁡ c ↔ x ∈ M ⁡ b
26 25 rspcev ⊢ b ∈ A ∧ x ∈ M ⁡ b → ∃ c ∈ A x ∈ M ⁡ c
27 21 23 26 syl2anc ⊢ Lim ⁡ A ∧ A ∈ V ∧ b ∈ A ∧ x ∈ Old ⁡ b → ∃ c ∈ A x ∈ M ⁡ c
28 27 rexlimdvaa ⊢ Lim ⁡ A ∧ A ∈ V → ∃ b ∈ A x ∈ Old ⁡ b → ∃ c ∈ A x ∈ M ⁡ c
29 20 28 impbid ⊢ Lim ⁡ A ∧ A ∈ V → ∃ c ∈ A x ∈ M ⁡ c ↔ ∃ b ∈ A x ∈ Old ⁡ b
30 elold ⊢ A ∈ On → x ∈ Old ⁡ A ↔ ∃ c ∈ A x ∈ M ⁡ c
31 10 30 syl ⊢ Lim ⁡ A ∧ A ∈ V → x ∈ Old ⁡ A ↔ ∃ c ∈ A x ∈ M ⁡ c
32 eliun ⊢ x ∈ ⋃ b ∈ A Old ⁡ b ↔ ∃ b ∈ A x ∈ Old ⁡ b
33 32 a1i ⊢ Lim ⁡ A ∧ A ∈ V → x ∈ ⋃ b ∈ A Old ⁡ b ↔ ∃ b ∈ A x ∈ Old ⁡ b
34 29 31 33 3bitr4d ⊢ Lim ⁡ A ∧ A ∈ V → x ∈ Old ⁡ A ↔ x ∈ ⋃ b ∈ A Old ⁡ b
35 34 eqrdv ⊢ Lim ⁡ A ∧ A ∈ V → Old ⁡ A = ⋃ b ∈ A Old ⁡ b
36 oldf ⊢ Old : On ⟶ 𝒫 No
37 ffun ⊢ Old : On ⟶ 𝒫 No → Fun ⁡ Old
38 funiunfv ⊢ Fun ⁡ Old → ⋃ b ∈ A Old ⁡ b = ⋃ Old A
39 36 37 38 mp2b ⊢ ⋃ b ∈ A Old ⁡ b = ⋃ Old A
40 35 39 eqtrdi ⊢ Lim ⁡ A ∧ A ∈ V → Old ⁡ A = ⋃ Old A