Step | Hyp | Ref
| Expression |
1 | | simp3 1140 |
. 2
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → 𝑋 ∈
ω) |
2 | | eleq1 2825 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥 ∈ ω ↔ 𝑋 ∈ ω)) |
3 | 2 | 3anbi3d 1444 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω))) |
4 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑁 +o 𝑥) = (𝑁 +o 𝑋)) |
5 | 4 | fveq2d 6721 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋))) |
6 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑀 +o 𝑥) = (𝑀 +o 𝑋)) |
7 | 6 | fveq2d 6721 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))) |
8 | 5, 7 | eqeq12d 2753 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋)))) |
9 | 8 | imbi2d 344 |
. . . 4
⊢ (𝑥 = 𝑋 → (((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))))) |
10 | 3, 9 | imbi12d 348 |
. . 3
⊢ (𝑥 = 𝑋 → (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋)))))) |
11 | | peano1 7667 |
. . . . 5
⊢ ∅
∈ ω |
12 | | oa0 8243 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ On → (𝑁 +o ∅) = 𝑁) |
13 | 12 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ On → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐴)‘𝑁)) |
14 | 13 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑁 ∈ On → (rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐴)‘(𝑁 +o ∅))) |
15 | | oa0 8243 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ On → (𝑀 +o ∅) = 𝑀) |
16 | 15 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ On → (rec(𝐹, 𝐵)‘(𝑀 +o ∅)) = (rec(𝐹, 𝐵)‘𝑀)) |
17 | 16 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝑀 ∈ On → (rec(𝐹, 𝐵)‘𝑀) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅))) |
18 | 14, 17 | eqeqan12d 2751 |
. . . . . . . . 9
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅)))) |
19 | 18 | biimpd 232 |
. . . . . . . 8
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅)))) |
20 | | eleq1 2825 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑥 ∈ ω ↔ ∅
∈ ω)) |
21 | 20 | 3anbi3d 1444 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ ∅ ∈
ω))) |
22 | 11 | biantru 533 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ On ↔ (𝑀 ∈ On ∧ ∅ ∈
ω)) |
23 | 22 | anbi2i 626 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) ↔ (𝑁 ∈ On ∧ (𝑀 ∈ On ∧ ∅ ∈
ω))) |
24 | | 3anass 1097 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ ∅ ∈
ω) ↔ (𝑁 ∈
On ∧ (𝑀 ∈ On ∧
∅ ∈ ω))) |
25 | 23, 24 | bitr4i 281 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ ∅ ∈
ω)) |
26 | 21, 25 | bitr4di 292 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On))) |
27 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑁 +o 𝑥) = (𝑁 +o ∅)) |
28 | 27 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o ∅))) |
29 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑀 +o 𝑥) = (𝑀 +o ∅)) |
30 | 29 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅))) |
31 | 28, 30 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅)))) |
32 | 31 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o ∅))))) |
33 | 26, 32 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o ∅)) = (rec(𝐹, 𝐵)‘(𝑀 +o
∅)))))) |
34 | 19, 33 | mpbiri 261 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) |
35 | 34 | ax-gen 1803 |
. . . . . 6
⊢
∀𝑥(𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) |
36 | | sbc6g 3724 |
. . . . . 6
⊢ (∅
∈ ω → ([∅ / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ∀𝑥(𝑥 = ∅ → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))))) |
37 | 35, 36 | mpbiri 261 |
. . . . 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 7661 |
. . . . 5
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) |
40 | 39 | 3anbi3i 1161 |
. . . . . . . 8
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈
ω)) |
41 | 40 | imbi1i 353 |
. . . . . . 7
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) |
42 | | nnon 7650 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
43 | | oacl 8262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ On ∧ 𝑥 ∈ On) → (𝑁 +o 𝑥) ∈ On) |
44 | | oacl 8262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ On ∧ 𝑥 ∈ On) → (𝑀 +o 𝑥) ∈ On) |
45 | 43, 44 | anim12i 616 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ On ∧ 𝑥 ∈ On) ∧ (𝑀 ∈ On ∧ 𝑥 ∈ On)) → ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) |
46 | 45 | 3impdir 1353 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On) → ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) |
47 | | rdgsuc 8160 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 +o 𝑥) ∈ On → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (𝐹‘(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)))) |
48 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . 18
⊢
((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) → (𝐹‘(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥))) = (𝐹‘(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) |
49 | 47, 48 | sylan9eqr 2800 |
. . . . . . . . . . . . . . . . 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 8160 |
. . . . . . . . . . . . . . . . 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 2780 |
. . . . . . . . . . . . . . 15
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ ((𝑁 +o 𝑥) ∈ On ∧ (𝑀 +o 𝑥) ∈ On)) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
54 | 46, 53 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢
(((rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ∧ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On)) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
55 | 54 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On) ∧ (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
56 | 42, 55 | syl3anl3 1416 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
57 | | onasuc 8255 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ On ∧ 𝑥 ∈ ω) → (𝑁 +o suc 𝑥) = suc (𝑁 +o 𝑥)) |
58 | 57 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥))) |
59 | 58 | 3adant2 1133 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥))) |
60 | 59 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐴)‘suc (𝑁 +o 𝑥))) |
61 | | onasuc 8255 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ On ∧ 𝑥 ∈ ω) → (𝑀 +o suc 𝑥) = suc (𝑀 +o 𝑥)) |
62 | 61 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
63 | 62 | 3adant1 1132 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
(rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
64 | 63 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘suc (𝑀 +o 𝑥))) |
65 | 56, 60, 64 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ∧
(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))) |
66 | 65 | ex 416 |
. . . . . . . . . 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 238 |
. . . . . . . 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 220 |
. . . . . 6
⊢ (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) |
71 | | sbcimg 3745 |
. . . . . . 7
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) ↔ ([suc 𝑥 / 𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → [suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))))) |
72 | | sbc3an 3765 |
. . . . . . . . 9
⊢
([suc 𝑥 /
𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ ([suc 𝑥 / 𝑥]𝑁 ∈ On ∧ [suc 𝑥 / 𝑥]𝑀 ∈ On ∧ [suc 𝑥 / 𝑥]𝑥 ∈ ω)) |
73 | | sbcg 3774 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]𝑁 ∈ On ↔ 𝑁 ∈ On)) |
74 | | sbcg 3774 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]𝑀 ∈ On ↔ 𝑀 ∈ On)) |
75 | | sbcel1v 3766 |
. . . . . . . . . . 11
⊢
([suc 𝑥 /
𝑥]𝑥 ∈ ω ↔ suc 𝑥 ∈ ω) |
76 | 75 | a1i 11 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)) |
77 | 73, 74, 76 | 3anbi123d 1438 |
. . . . . . . . 9
⊢ (suc
𝑥 ∈ ω →
(([suc 𝑥 / 𝑥]𝑁 ∈ On ∧ [suc 𝑥 / 𝑥]𝑀 ∈ On ∧ [suc 𝑥 / 𝑥]𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω))) |
78 | 72, 77 | syl5bb 286 |
. . . . . . . 8
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) ↔ (𝑁 ∈ On ∧ 𝑀 ∈ On ∧ suc 𝑥 ∈ ω))) |
79 | | sbcimg 3745 |
. . . . . . . . 9
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → [suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) |
80 | | sbcg 3774 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) ↔ (rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀))) |
81 | | sbceqg 4324 |
. . . . . . . . . . 11
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ ⦋suc 𝑥 / 𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = ⦋suc 𝑥 / 𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) |
82 | | csbfv12 6760 |
. . . . . . . . . . . . 13
⊢
⦋suc 𝑥
/ 𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (⦋suc 𝑥 / 𝑥⦌rec(𝐹, 𝐴)‘⦋suc 𝑥 / 𝑥⦌(𝑁 +o 𝑥)) |
83 | | csbconstg 3830 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐴) = rec(𝐹, 𝐴)) |
84 | | csbov123 7255 |
. . . . . . . . . . . . . . 15
⊢
⦋suc 𝑥
/ 𝑥⦌(𝑁 +o 𝑥) = (⦋suc 𝑥 / 𝑥⦌𝑁⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) |
85 | | csbconstg 3830 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌
+o = +o ) |
86 | | csbconstg 3830 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌𝑁 = 𝑁) |
87 | | csbvarg 4346 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌𝑥 = suc 𝑥) |
88 | 85, 86, 87 | oveq123d 7234 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌𝑁⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) = (𝑁 +o suc 𝑥)) |
89 | 84, 88 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(𝑁 +o 𝑥) = (𝑁 +o suc 𝑥)) |
90 | 83, 89 | fveq12d 6724 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐴)‘⦋suc 𝑥 / 𝑥⦌(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥))) |
91 | 82, 90 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥))) |
92 | | csbfv12 6760 |
. . . . . . . . . . . . 13
⊢
⦋suc 𝑥
/ 𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (⦋suc 𝑥 / 𝑥⦌rec(𝐹, 𝐵)‘⦋suc 𝑥 / 𝑥⦌(𝑀 +o 𝑥)) |
93 | | csbconstg 3830 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐵) = rec(𝐹, 𝐵)) |
94 | | csbov123 7255 |
. . . . . . . . . . . . . . 15
⊢
⦋suc 𝑥
/ 𝑥⦌(𝑀 +o 𝑥) = (⦋suc 𝑥 / 𝑥⦌𝑀⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) |
95 | | csbconstg 3830 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌𝑀 = 𝑀) |
96 | 85, 95, 87 | oveq123d 7234 |
. . . . . . . . . . . . . . 15
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌𝑀⦋suc 𝑥 / 𝑥⦌ +o
⦋suc 𝑥 /
𝑥⦌𝑥) = (𝑀 +o suc 𝑥)) |
97 | 94, 96 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(𝑀 +o 𝑥) = (𝑀 +o suc 𝑥)) |
98 | 93, 97 | fveq12d 6724 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌rec(𝐹, 𝐵)‘⦋suc 𝑥 / 𝑥⦌(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))) |
99 | 92, 98 | syl5eq 2790 |
. . . . . . . . . . . 12
⊢ (suc
𝑥 ∈ ω →
⦋suc 𝑥 /
𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))) |
100 | 91, 99 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (suc
𝑥 ∈ ω →
(⦋suc 𝑥 /
𝑥⦌(rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = ⦋suc 𝑥 / 𝑥⦌(rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))) |
101 | 81, 100 | bitrd 282 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)) ↔ (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥)))) |
102 | 80, 101 | imbi12d 348 |
. . . . . . . . 9
⊢ (suc
𝑥 ∈ ω →
(([suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → [suc 𝑥 / 𝑥](rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) |
103 | 79, 102 | bitrd 282 |
. . . . . . . 8
⊢ (suc
𝑥 ∈ ω →
([suc 𝑥 / 𝑥]((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))) ↔ ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o suc 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o suc 𝑥))))) |
104 | 78, 103 | imbi12d 348 |
. . . . . . 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 282 |
. . . . . 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 | syl5ibr 249 |
. . . . 5
⊢ (suc
𝑥 ∈ ω →
(((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → [suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))))) |
107 | 39, 106 | sylbi 220 |
. . . 4
⊢ (𝑥 ∈ ω → (((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))) → [suc 𝑥 / 𝑥]((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥)))))) |
108 | 38, 107 | findes 7680 |
. . 3
⊢ (𝑥 ∈ ω → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑥)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑥))))) |
109 | 10, 108 | vtoclga 3489 |
. 2
⊢ (𝑋 ∈ ω → ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋))))) |
110 | 1, 109 | mpcom 38 |
1
⊢ ((𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω) →
((rec(𝐹, 𝐴)‘𝑁) = (rec(𝐹, 𝐵)‘𝑀) → (rec(𝐹, 𝐴)‘(𝑁 +o 𝑋)) = (rec(𝐹, 𝐵)‘(𝑀 +o 𝑋)))) |