| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = ∅ → (𝐴 +o 𝑥) = (𝐴 +o ∅)) | 
| 2 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = ∅ → (𝐴 +no 𝑥) = (𝐴 +no ∅)) | 
| 3 | 1, 2 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = ∅ → ((𝐴 +o 𝑥) = (𝐴 +no 𝑥) ↔ (𝐴 +o ∅) = (𝐴 +no ∅))) | 
| 4 | 3 | imbi2d 340 | . . 3
⊢ (𝑥 = ∅ → ((𝐴 ∈ On → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) ↔ (𝐴 ∈ On → (𝐴 +o ∅) = (𝐴 +no ∅)))) | 
| 5 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 +o 𝑥) = (𝐴 +o 𝑦)) | 
| 6 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 +no 𝑥) = (𝐴 +no 𝑦)) | 
| 7 | 5, 6 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 +o 𝑥) = (𝐴 +no 𝑥) ↔ (𝐴 +o 𝑦) = (𝐴 +no 𝑦))) | 
| 8 | 7 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ On → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) ↔ (𝐴 ∈ On → (𝐴 +o 𝑦) = (𝐴 +no 𝑦)))) | 
| 9 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 +o 𝑥) = (𝐴 +o suc 𝑦)) | 
| 10 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 +no 𝑥) = (𝐴 +no suc 𝑦)) | 
| 11 | 9, 10 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐴 +o 𝑥) = (𝐴 +no 𝑥) ↔ (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦))) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑥 = suc 𝑦 → ((𝐴 ∈ On → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) ↔ (𝐴 ∈ On → (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦)))) | 
| 13 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 +o 𝑥) = (𝐴 +o 𝐵)) | 
| 14 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 +no 𝑥) = (𝐴 +no 𝐵)) | 
| 15 | 13, 14 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝐵 → ((𝐴 +o 𝑥) = (𝐴 +no 𝑥) ↔ (𝐴 +o 𝐵) = (𝐴 +no 𝐵))) | 
| 16 | 15 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ On → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) ↔ (𝐴 ∈ On → (𝐴 +o 𝐵) = (𝐴 +no 𝐵)))) | 
| 17 |  | oa0 8555 | . . . 4
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = 𝐴) | 
| 18 |  | naddrid 8722 | . . . 4
⊢ (𝐴 ∈ On → (𝐴 +no ∅) = 𝐴) | 
| 19 | 17, 18 | eqtr4d 2779 | . . 3
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = (𝐴 +no ∅)) | 
| 20 |  | nnon 7894 | . . . . 5
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) | 
| 21 |  | suceq 6449 | . . . . . . . . 9
⊢ ((𝐴 +o 𝑦) = (𝐴 +no 𝑦) → suc (𝐴 +o 𝑦) = suc (𝐴 +no 𝑦)) | 
| 22 | 21 | adantl 481 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 +o 𝑦) = (𝐴 +no 𝑦)) → suc (𝐴 +o 𝑦) = suc (𝐴 +no 𝑦)) | 
| 23 |  | oasuc 8563 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +o suc 𝑦) = suc (𝐴 +o 𝑦)) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 +o 𝑦) = (𝐴 +no 𝑦)) → (𝐴 +o suc 𝑦) = suc (𝐴 +o 𝑦)) | 
| 25 |  | naddsuc2 8740 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +no suc 𝑦) = suc (𝐴 +no 𝑦)) | 
| 26 | 25 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 +o 𝑦) = (𝐴 +no 𝑦)) → (𝐴 +no suc 𝑦) = suc (𝐴 +no 𝑦)) | 
| 27 | 22, 24, 26 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ (𝐴 +o 𝑦) = (𝐴 +no 𝑦)) → (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦)) | 
| 28 | 27 | ex 412 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +o 𝑦) = (𝐴 +no 𝑦) → (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦))) | 
| 29 | 28 | expcom 413 | . . . . 5
⊢ (𝑦 ∈ On → (𝐴 ∈ On → ((𝐴 +o 𝑦) = (𝐴 +no 𝑦) → (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦)))) | 
| 30 | 20, 29 | syl 17 | . . . 4
⊢ (𝑦 ∈ ω → (𝐴 ∈ On → ((𝐴 +o 𝑦) = (𝐴 +no 𝑦) → (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦)))) | 
| 31 | 30 | a2d 29 | . . 3
⊢ (𝑦 ∈ ω → ((𝐴 ∈ On → (𝐴 +o 𝑦) = (𝐴 +no 𝑦)) → (𝐴 ∈ On → (𝐴 +o suc 𝑦) = (𝐴 +no suc 𝑦)))) | 
| 32 | 4, 8, 12, 16, 19, 31 | finds 7919 | . 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ On → (𝐴 +o 𝐵) = (𝐴 +no 𝐵))) | 
| 33 | 32 | impcom 407 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐴 +no 𝐵)) |