Metamath Proof Explorer

Theorem madeoldsuc

Description: The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion madeoldsuc ⊢ A ∈ On → M ⁡ A = Old ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc ⁡ A = A ∪ A
2 1 imaeq2i ⊢ M suc ⁡ A = M A ∪ A
3 imaundi ⊢ M A ∪ A = M A ∪ M A
4 2 3 eqtri ⊢ M suc ⁡ A = M A ∪ M A
5 4 unieqi ⊢ ⋃ M suc ⁡ A = ⋃ M A ∪ M A
6 uniun ⊢ ⋃ M A ∪ M A = ⋃ M A ∪ ⋃ M A
7 5 6 eqtri ⊢ ⋃ M suc ⁡ A = ⋃ M A ∪ ⋃ M A
8 7 a1i ⊢ A ∈ On → ⋃ M suc ⁡ A = ⋃ M A ∪ ⋃ M A
9 oldval ⊢ A ∈ On → Old ⁡ A = ⋃ M A
10 9 eqcomd ⊢ A ∈ On → ⋃ M A = Old ⁡ A
11 madef ⊢ M : On ⟶ 𝒫 No
12 ffn ⊢ M : On ⟶ 𝒫 No → M Fn On
13 11 12 ax-mp ⊢ M Fn On
14 fnsnfv ⊢ M Fn On ∧ A ∈ On → M ⁡ A = M A
15 14 eqcomd ⊢ M Fn On ∧ A ∈ On → M A = M ⁡ A
16 13 15 mpan ⊢ A ∈ On → M A = M ⁡ A
17 16 unieqd ⊢ A ∈ On → ⋃ M A = ⋃ M ⁡ A
18 fvex ⊢ M ⁡ A ∈ V
19 18 unisn ⊢ ⋃ M ⁡ A = M ⁡ A
20 17 19 eqtrdi ⊢ A ∈ On → ⋃ M A = M ⁡ A
21 10 20 uneq12d ⊢ A ∈ On → ⋃ M A ∪ ⋃ M A = Old ⁡ A ∪ M ⁡ A
22 oldssmade ⊢ A ∈ On → Old ⁡ A ⊆ M ⁡ A
23 ssequn1 ⊢ Old ⁡ A ⊆ M ⁡ A ↔ Old ⁡ A ∪ M ⁡ A = M ⁡ A
24 22 23 sylib ⊢ A ∈ On → Old ⁡ A ∪ M ⁡ A = M ⁡ A
25 8 21 24 3eqtrrd ⊢ A ∈ On → M ⁡ A = ⋃ M suc ⁡ A
26 suceloni ⊢ A ∈ On → suc ⁡ A ∈ On
27 oldval ⊢ suc ⁡ A ∈ On → Old ⁡ suc ⁡ A = ⋃ M suc ⁡ A
28 26 27 syl ⊢ A ∈ On → Old ⁡ suc ⁡ A = ⋃ M suc ⁡ A
29 25 28 eqtr4d ⊢ A ∈ On → M ⁡ A = Old ⁡ suc ⁡ A