| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp3 1138 | . 2
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → 𝑋 ∈
ω) | 
| 2 |  | eleq1 2828 | . . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ω ↔ 𝑋 ∈ ω)) | 
| 3 | 2 | 3anbi3d 1443 | . . . 4
⊢ (𝑥 = 𝑋 → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω))) | 
| 4 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑁 +o 𝑥) = (𝑁 +o 𝑋)) | 
| 5 | 4 | fveq2d 6909 | . . . . . 6
⊢ (𝑥 = 𝑋 → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋))) | 
| 6 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑀 +o 𝑥) = (𝑀 +o 𝑋)) | 
| 7 | 6 | fveq2d 6909 | . . . . . 6
⊢ (𝑥 = 𝑋 → (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))) | 
| 8 | 5, 7 | eqeq12d 2752 | . . . . 5
⊢ (𝑥 = 𝑋 → ((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋)))) | 
| 9 | 8 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑋 → (((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))))) | 
| 10 | 3, 9 | imbi12d 344 | . . 3
⊢ (𝑥 = 𝑋 → (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋)))))) | 
| 11 |  | peano1 7911 | . . . . 5
⊢ ∅
∈ ω | 
| 12 |  | oa0 8555 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ On → (𝑁 +o ∅) = 𝑁) | 
| 13 | 12 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑁 ∈ On → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐴)‘𝑁)) | 
| 14 | 13 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝑁 ∈ On → (rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐴)‘(𝑁 +o ∅))) | 
| 15 |  | oa0 8555 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ On → (𝑀 +o ∅) = 𝑀) | 
| 16 | 15 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑀 ∈ On → (rec(𝐹, 𝐵)‘(𝑀 +o ∅)) = (rec(𝐹, 𝐵)‘𝑀)) | 
| 17 | 16 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝑀 ∈ On → (rec(𝐹, 𝐵)‘𝑀) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅))) | 
| 18 | 14, 17 | eqeqan12d 2750 | . . . . . . . . 9
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅)))) | 
| 19 | 18 | biimpd 229 | . . . . . . . 8
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅)))) | 
| 20 |  | eleq1 2828 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 ∈ ω ↔ ∅
∈ ω)) | 
| 21 | 20 | 3anbi3d 1443 | . . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ ∅ ∈
ω))) | 
| 22 | 11 | biantru 529 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ On ↔ (𝑀 ∈ On ∧ ∅ ∈
ω)) | 
| 23 | 22 | anbi2i 623 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) ↔ (𝑁 ∈ On ∧ (𝑀 ∈ On ∧ ∅ ∈
ω))) | 
| 24 |  | 3anass 1094 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ ∅ ∈
ω) ↔ (𝑁 ∈
On ∧ (𝑀 ∈ On ∧
∅ ∈ ω))) | 
| 25 | 23, 24 | bitr4i 278 | . . . . . . . . . 10
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ ∅ ∈
ω)) | 
| 26 | 21, 25 | bitr4di 289 | . . . . . . . . 9
⊢ (𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On))) | 
| 27 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑁 +o 𝑥) = (𝑁 +o ∅)) | 
| 28 | 27 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o ∅))) | 
| 29 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑀 +o 𝑥) = (𝑀 +o ∅)) | 
| 30 | 29 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅))) | 
| 31 | 28, 30 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅)))) | 
| 32 | 31 | imbi2d 340 | . . . . . . . . 9
⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅))))) | 
| 33 | 26, 32 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = ∅ → (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o
∅)))))) | 
| 34 | 19, 33 | mpbiri 258 | . . . . . . 7
⊢ (𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) | 
| 35 | 34 | ax-gen 1794 | . . . . . 6
⊢
∀𝑥(𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) | 
| 36 |  | sbc6g 3817 | . . . . . 6
⊢ (∅
∈ ω → ([∅ / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ∀𝑥(𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))))) | 
| 37 | 35, 36 | mpbiri 258 | . . . . 5
⊢ (∅
∈ ω → [∅ / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) | 
| 38 | 11, 37 | ax-mp 5 | . . . 4
⊢
[∅ / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 39 |  | peano2b 7905 | . . . . 5
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) | 
| 40 | 39 | 3anbi3i 1159 | . . . . . . . 8
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈
ω)) | 
| 41 | 40 | imbi1i 349 | . . . . . . 7
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) | 
| 42 |  | nnon 7894 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) | 
| 43 |  | oacl 8574 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ On ∧ 𝑥 ∈ On) → (𝑁 +o 𝑥) ∈ On) | 
| 44 |  | oacl 8574 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ On ∧ 𝑥 ∈ On) → (𝑀 +o 𝑥) ∈ On) | 
| 45 | 43, 44 | anim12i 613 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑀 ∈ On ∧ 𝑥 ∈ On)) → ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) | 
| 46 | 45 | 3impdir 1351 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On) → ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) | 
| 47 |  | rdgsuc 8465 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 +o 𝑥) ∈ On → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (𝐹‘(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)))) | 
| 48 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢
((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) → (𝐹‘(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥))) = (𝐹‘(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 49 | 47, 48 | sylan9eqr 2798 | . . . . . . . . . . . . . . . . 17
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ (𝑁 +o 𝑥) ∈ On) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (𝐹‘(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 50 | 49 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (𝐹‘(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 51 |  | rdgsuc 8465 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 +o 𝑥) ∈ On → (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥)) = (𝐹‘(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 52 | 51 | ad2antll 729 | . . . . . . . . . . . . . . . 16
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) → (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥)) = (𝐹‘(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 53 | 50, 52 | eqtr4d 2779 | . . . . . . . . . . . . . . 15
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 54 | 46, 53 | sylan2 593 | . . . . . . . . . . . . . 14
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On)) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 55 | 54 | ancoms 458 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On) ∧ (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 56 | 42, 55 | syl3anl3 1415 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 57 |  | onasuc 8567 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ On ∧ 𝑥 ∈ ω) → (𝑁 +o suc 𝑥) = suc (𝑁 +o 𝑥)) | 
| 58 | 57 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥))) | 
| 59 | 58 | 3adant2 1131 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥))) | 
| 60 | 59 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥))) | 
| 61 |  | onasuc 8567 | . . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ On ∧ 𝑥 ∈ ω) → (𝑀 +o suc 𝑥) = suc (𝑀 +o 𝑥)) | 
| 62 | 61 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 63 | 62 | 3adant1 1130 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) | 
| 65 | 56, 60, 64 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))) | 
| 66 | 65 | ex 412 | . . . . . . . . . 10
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))) | 
| 67 | 66 | imim2d 57 | . . . . . . . . 9
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) | 
| 68 | 40, 67 | sylbir 235 | . . . . . . . 8
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) →
(((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) | 
| 69 | 68 | a2i 14 | . . . . . . 7
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) | 
| 70 | 41, 69 | sylbi 217 | . . . . . 6
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) | 
| 71 |  | sbcimg 3836 | . . . . . . 7
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ([suc 𝑥 / 𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → [suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))))) | 
| 72 |  | sbc3an 3854 | . . . . . . . . 9
⊢
([suc 𝑥 /
𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ ([suc 𝑥 / 𝑥]𝑁 ∈ On ∧ [suc 𝑥 / 𝑥]𝑀 ∈ On ∧ [suc 𝑥 / 𝑥]𝑥 ∈ ω)) | 
| 73 |  | sbcg 3862 | . . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]𝑁 ∈ On ↔ 𝑁 ∈ On)) | 
| 74 |  | sbcg 3862 | . . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]𝑀 ∈ On ↔ 𝑀 ∈ On)) | 
| 75 |  | sbcel1v 3855 | . . . . . . . . . . 11
⊢
([suc 𝑥 /
𝑥]𝑥 ∈ ω ↔ suc 𝑥 ∈ ω) | 
| 76 | 75 | a1i 11 | . . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)) | 
| 77 | 73, 74, 76 | 3anbi123d 1437 | . . . . . . . . 9
⊢ (suc
𝑥 ∈ ω →
(([suc 𝑥 / 𝑥]𝑁 ∈ On ∧ [suc 𝑥 / 𝑥]𝑀 ∈ On ∧ [suc 𝑥 / 𝑥]𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω))) | 
| 78 | 72, 77 | bitrid 283 | . . . . . . . 8
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω))) | 
| 79 |  | sbcimg 3836 | . . . . . . . . 9
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → [suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) | 
| 80 |  | sbcg 3862 | . . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) ↔ (rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀))) | 
| 81 |  | sbceqg 4411 | . . . . . . . . . . 11
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ ⦋suc 𝑥 / 𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = ⦋suc 𝑥 / 𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) | 
| 82 |  | csbfv12 6953 | . . . . . . . . . . . . 13
⊢
⦋suc 𝑥
/ 𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (⦋suc 𝑥 / 𝑥⦌rec(𝐹, 𝐴)‘⦋suc 𝑥 / 𝑥⦌(𝑁 +o 𝑥)) | 
| 83 |  | csbconstg 3917 | . . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐴) = rec(𝐹, 𝐴)) | 
| 84 |  | csbov123 7476 | . . . . . . . . . . . . . . 15
⊢
⦋suc 𝑥
/ 𝑥⦌(𝑁 +o 𝑥) = (⦋suc 𝑥 / 𝑥⦌𝑁⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) | 
| 85 |  | csbconstg 3917 | . . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌
+o = +o ) | 
| 86 |  | csbconstg 3917 | . . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌𝑁 = 𝑁) | 
| 87 |  | csbvarg 4433 | . . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌𝑥 = suc 𝑥) | 
| 88 | 85, 86, 87 | oveq123d 7453 | . . . . . . . . . . . . . . 15
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌𝑁⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) = (𝑁 +o suc 𝑥)) | 
| 89 | 84, 88 | eqtrid 2788 | . . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(𝑁 +o 𝑥) = (𝑁 +o suc 𝑥)) | 
| 90 | 83, 89 | fveq12d 6912 | . . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐴)‘⦋suc 𝑥 / 𝑥⦌(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥))) | 
| 91 | 82, 90 | eqtrid 2788 | . . . . . . . . . . . 12
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥))) | 
| 92 |  | csbfv12 6953 | . . . . . . . . . . . . 13
⊢
⦋suc 𝑥
/ 𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (⦋suc 𝑥 / 𝑥⦌rec(𝐹, 𝐵)‘⦋suc 𝑥 / 𝑥⦌(𝑀 +o 𝑥)) | 
| 93 |  | csbconstg 3917 | . . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐵) = rec(𝐹, 𝐵)) | 
| 94 |  | csbov123 7476 | . . . . . . . . . . . . . . 15
⊢
⦋suc 𝑥
/ 𝑥⦌(𝑀 +o 𝑥) = (⦋suc 𝑥 / 𝑥⦌𝑀⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) | 
| 95 |  | csbconstg 3917 | . . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌𝑀 = 𝑀) | 
| 96 | 85, 95, 87 | oveq123d 7453 | . . . . . . . . . . . . . . 15
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌𝑀⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) = (𝑀 +o suc 𝑥)) | 
| 97 | 94, 96 | eqtrid 2788 | . . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(𝑀 +o 𝑥) = (𝑀 +o suc 𝑥)) | 
| 98 | 93, 97 | fveq12d 6912 | . . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐵)‘⦋suc 𝑥 / 𝑥⦌(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))) | 
| 99 | 92, 98 | eqtrid 2788 | . . . . . . . . . . . 12
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))) | 
| 100 | 91, 99 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = ⦋suc 𝑥 / 𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))) | 
| 101 | 81, 100 | bitrd 279 | . . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))) | 
| 102 | 80, 101 | imbi12d 344 | . . . . . . . . 9
⊢ (suc
𝑥 ∈ ω →
(([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → [suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) | 
| 103 | 79, 102 | bitrd 279 | . . . . . . . 8
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) | 
| 104 | 78, 103 | imbi12d 344 | . . . . . . 7
⊢ (suc
𝑥 ∈ ω →
(([suc 𝑥 / 𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → [suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))))) | 
| 105 | 71, 104 | bitrd 279 | . . . . . 6
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))))) | 
| 106 | 70, 105 | imbitrrid 246 | . . . . 5
⊢ (suc
𝑥 ∈ ω →
(((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → [suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))))) | 
| 107 | 39, 106 | sylbi 217 | . . . 4
⊢ (𝑥 ∈ ω → (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → [suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))))) | 
| 108 | 38, 107 | findes 7923 | . . 3
⊢ (𝑥 ∈ ω → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) | 
| 109 | 10, 108 | vtoclga 3576 | . 2
⊢ (𝑋 ∈ ω → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))))) | 
| 110 | 1, 109 | mpcom 38 | 1
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋)))) |