| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . 6
⊢ (𝑛 = ∅ → (𝐴 +o 𝑛) = (𝐴 +o ∅)) | 
| 2 | 1 | fveq2d 6910 | . . . . 5
⊢ (𝑛 = ∅ → (𝐺‘(𝐴 +o 𝑛)) = (𝐺‘(𝐴 +o ∅))) | 
| 3 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = ∅ → (𝐺‘𝑛) = (𝐺‘∅)) | 
| 4 | 3 | oveq2d 7447 | . . . . 5
⊢ (𝑛 = ∅ → ((𝐺‘𝐴) + (𝐺‘𝑛)) = ((𝐺‘𝐴) + (𝐺‘∅))) | 
| 5 | 2, 4 | eqeq12d 2753 | . . . 4
⊢ (𝑛 = ∅ → ((𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛)) ↔ (𝐺‘(𝐴 +o ∅)) = ((𝐺‘𝐴) + (𝐺‘∅)))) | 
| 6 | 5 | imbi2d 340 | . . 3
⊢ (𝑛 = ∅ → ((𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛))) ↔ (𝐴 ∈ ω → (𝐺‘(𝐴 +o ∅)) = ((𝐺‘𝐴) + (𝐺‘∅))))) | 
| 7 |  | oveq2 7439 | . . . . . 6
⊢ (𝑛 = 𝑧 → (𝐴 +o 𝑛) = (𝐴 +o 𝑧)) | 
| 8 | 7 | fveq2d 6910 | . . . . 5
⊢ (𝑛 = 𝑧 → (𝐺‘(𝐴 +o 𝑛)) = (𝐺‘(𝐴 +o 𝑧))) | 
| 9 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = 𝑧 → (𝐺‘𝑛) = (𝐺‘𝑧)) | 
| 10 | 9 | oveq2d 7447 | . . . . 5
⊢ (𝑛 = 𝑧 → ((𝐺‘𝐴) + (𝐺‘𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) | 
| 11 | 8, 10 | eqeq12d 2753 | . . . 4
⊢ (𝑛 = 𝑧 → ((𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛)) ↔ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧)))) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝑧 → ((𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛))) ↔ (𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))))) | 
| 13 |  | oveq2 7439 | . . . . . 6
⊢ (𝑛 = suc 𝑧 → (𝐴 +o 𝑛) = (𝐴 +o suc 𝑧)) | 
| 14 | 13 | fveq2d 6910 | . . . . 5
⊢ (𝑛 = suc 𝑧 → (𝐺‘(𝐴 +o 𝑛)) = (𝐺‘(𝐴 +o suc 𝑧))) | 
| 15 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = suc 𝑧 → (𝐺‘𝑛) = (𝐺‘suc 𝑧)) | 
| 16 | 15 | oveq2d 7447 | . . . . 5
⊢ (𝑛 = suc 𝑧 → ((𝐺‘𝐴) + (𝐺‘𝑛)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧))) | 
| 17 | 14, 16 | eqeq12d 2753 | . . . 4
⊢ (𝑛 = suc 𝑧 → ((𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛)) ↔ (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧)))) | 
| 18 | 17 | imbi2d 340 | . . 3
⊢ (𝑛 = suc 𝑧 → ((𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛))) ↔ (𝐴 ∈ ω → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧))))) | 
| 19 |  | oveq2 7439 | . . . . . 6
⊢ (𝑛 = 𝐵 → (𝐴 +o 𝑛) = (𝐴 +o 𝐵)) | 
| 20 | 19 | fveq2d 6910 | . . . . 5
⊢ (𝑛 = 𝐵 → (𝐺‘(𝐴 +o 𝑛)) = (𝐺‘(𝐴 +o 𝐵))) | 
| 21 |  | fveq2 6906 | . . . . . 6
⊢ (𝑛 = 𝐵 → (𝐺‘𝑛) = (𝐺‘𝐵)) | 
| 22 | 21 | oveq2d 7447 | . . . . 5
⊢ (𝑛 = 𝐵 → ((𝐺‘𝐴) + (𝐺‘𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝐵))) | 
| 23 | 20, 22 | eqeq12d 2753 | . . . 4
⊢ (𝑛 = 𝐵 → ((𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛)) ↔ (𝐺‘(𝐴 +o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵)))) | 
| 24 | 23 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝐵 → ((𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝑛)) = ((𝐺‘𝐴) + (𝐺‘𝑛))) ↔ (𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵))))) | 
| 25 |  | hashgadd.1 | . . . . . . . . 9
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) | 
| 26 | 25 | hashgf1o 14012 | . . . . . . . 8
⊢ 𝐺:ω–1-1-onto→ℕ0 | 
| 27 |  | f1of 6848 | . . . . . . . 8
⊢ (𝐺:ω–1-1-onto→ℕ0 → 𝐺:ω⟶ℕ0) | 
| 28 | 26, 27 | ax-mp 5 | . . . . . . 7
⊢ 𝐺:ω⟶ℕ0 | 
| 29 | 28 | ffvelcdmi 7103 | . . . . . 6
⊢ (𝐴 ∈ ω → (𝐺‘𝐴) ∈
ℕ0) | 
| 30 | 29 | nn0cnd 12589 | . . . . 5
⊢ (𝐴 ∈ ω → (𝐺‘𝐴) ∈ ℂ) | 
| 31 | 30 | addridd 11461 | . . . 4
⊢ (𝐴 ∈ ω → ((𝐺‘𝐴) + 0) = (𝐺‘𝐴)) | 
| 32 |  | 0z 12624 | . . . . . . 7
⊢ 0 ∈
ℤ | 
| 33 | 32, 25 | om2uz0i 13988 | . . . . . 6
⊢ (𝐺‘∅) =
0 | 
| 34 | 33 | oveq2i 7442 | . . . . 5
⊢ ((𝐺‘𝐴) + (𝐺‘∅)) = ((𝐺‘𝐴) + 0) | 
| 35 | 34 | a1i 11 | . . . 4
⊢ (𝐴 ∈ ω → ((𝐺‘𝐴) + (𝐺‘∅)) = ((𝐺‘𝐴) + 0)) | 
| 36 |  | nna0 8642 | . . . . 5
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) | 
| 37 | 36 | fveq2d 6910 | . . . 4
⊢ (𝐴 ∈ ω → (𝐺‘(𝐴 +o ∅)) = (𝐺‘𝐴)) | 
| 38 | 31, 35, 37 | 3eqtr4rd 2788 | . . 3
⊢ (𝐴 ∈ ω → (𝐺‘(𝐴 +o ∅)) = ((𝐺‘𝐴) + (𝐺‘∅))) | 
| 39 |  | nnasuc 8644 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → (𝐴 +o suc 𝑧) = suc (𝐴 +o 𝑧)) | 
| 40 | 39 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → (𝐺‘(𝐴 +o suc 𝑧)) = (𝐺‘suc (𝐴 +o 𝑧))) | 
| 41 |  | nnacl 8649 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → (𝐴 +o 𝑧) ∈
ω) | 
| 42 | 32, 25 | om2uzsuci 13989 | . . . . . . . . . 10
⊢ ((𝐴 +o 𝑧) ∈ ω → (𝐺‘suc (𝐴 +o 𝑧)) = ((𝐺‘(𝐴 +o 𝑧)) + 1)) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → (𝐺‘suc (𝐴 +o 𝑧)) = ((𝐺‘(𝐴 +o 𝑧)) + 1)) | 
| 44 | 40, 43 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘(𝐴 +o 𝑧)) + 1)) | 
| 45 | 44 | 3adant3 1133 | . . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘(𝐴 +o 𝑧)) + 1)) | 
| 46 | 28 | ffvelcdmi 7103 | . . . . . . . . . . 11
⊢ (𝑧 ∈ ω → (𝐺‘𝑧) ∈
ℕ0) | 
| 47 | 46 | nn0cnd 12589 | . . . . . . . . . 10
⊢ (𝑧 ∈ ω → (𝐺‘𝑧) ∈ ℂ) | 
| 48 |  | ax-1cn 11213 | . . . . . . . . . . 11
⊢ 1 ∈
ℂ | 
| 49 |  | addass 11242 | . . . . . . . . . . 11
⊢ (((𝐺‘𝐴) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝐺‘𝐴) + (𝐺‘𝑧)) + 1) = ((𝐺‘𝐴) + ((𝐺‘𝑧) + 1))) | 
| 50 | 48, 49 | mp3an3 1452 | . . . . . . . . . 10
⊢ (((𝐺‘𝐴) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (((𝐺‘𝐴) + (𝐺‘𝑧)) + 1) = ((𝐺‘𝐴) + ((𝐺‘𝑧) + 1))) | 
| 51 | 30, 47, 50 | syl2an 596 | . . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → (((𝐺‘𝐴) + (𝐺‘𝑧)) + 1) = ((𝐺‘𝐴) + ((𝐺‘𝑧) + 1))) | 
| 52 | 51 | 3adant3 1133 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → (((𝐺‘𝐴) + (𝐺‘𝑧)) + 1) = ((𝐺‘𝐴) + ((𝐺‘𝑧) + 1))) | 
| 53 |  | oveq1 7438 | . . . . . . . . 9
⊢ ((𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧)) → ((𝐺‘(𝐴 +o 𝑧)) + 1) = (((𝐺‘𝐴) + (𝐺‘𝑧)) + 1)) | 
| 54 | 53 | 3ad2ant3 1136 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → ((𝐺‘(𝐴 +o 𝑧)) + 1) = (((𝐺‘𝐴) + (𝐺‘𝑧)) + 1)) | 
| 55 | 32, 25 | om2uzsuci 13989 | . . . . . . . . . 10
⊢ (𝑧 ∈ ω → (𝐺‘suc 𝑧) = ((𝐺‘𝑧) + 1)) | 
| 56 | 55 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑧 ∈ ω → ((𝐺‘𝐴) + (𝐺‘suc 𝑧)) = ((𝐺‘𝐴) + ((𝐺‘𝑧) + 1))) | 
| 57 | 56 | 3ad2ant2 1135 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → ((𝐺‘𝐴) + (𝐺‘suc 𝑧)) = ((𝐺‘𝐴) + ((𝐺‘𝑧) + 1))) | 
| 58 | 52, 54, 57 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → ((𝐺‘(𝐴 +o 𝑧)) + 1) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧))) | 
| 59 | 45, 58 | eqtrd 2777 | . . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω ∧ (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧))) | 
| 60 | 59 | 3expia 1122 | . . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑧 ∈ ω) → ((𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧)) → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧)))) | 
| 61 | 60 | expcom 413 | . . . 4
⊢ (𝑧 ∈ ω → (𝐴 ∈ ω → ((𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧)) → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧))))) | 
| 62 | 61 | a2d 29 | . . 3
⊢ (𝑧 ∈ ω → ((𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝑧)) = ((𝐺‘𝐴) + (𝐺‘𝑧))) → (𝐴 ∈ ω → (𝐺‘(𝐴 +o suc 𝑧)) = ((𝐺‘𝐴) + (𝐺‘suc 𝑧))))) | 
| 63 | 6, 12, 18, 24, 38, 62 | finds 7918 | . 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (𝐺‘(𝐴 +o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵)))) | 
| 64 | 63 | impcom 407 | 1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐺‘(𝐴 +o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵))) |