Step | Hyp | Ref
| Expression |
1 | | nninffeq.f |
. . 3
⊢ (𝜑 → 𝐹:ℕ∞⟶ℕ0) |
2 | 1 | ffnd 5229 |
. 2
⊢ (𝜑 → 𝐹 Fn
ℕ∞) |
3 | | nninffeq.g |
. . 3
⊢ (𝜑 → 𝐺:ℕ∞⟶ℕ0) |
4 | 3 | ffnd 5229 |
. 2
⊢ (𝜑 → 𝐺 Fn
ℕ∞) |
5 | | eqid 2113 |
. . . . . . . 8
⊢ (𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) = (𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) |
6 | | fveq2 5373 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
7 | | fveq2 5373 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
8 | 6, 7 | eqeq12d 2127 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑧) = (𝐺‘𝑧))) |
9 | 8 | ifbid 3457 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) = if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅)) |
10 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
𝑧 ∈
ℕ∞) |
11 | | 1onn 6368 |
. . . . . . . . . 10
⊢
1o ∈ ω |
12 | 11 | a1i 9 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
1o ∈ ω) |
13 | | peano1 4466 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
14 | 13 | a1i 9 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
∅ ∈ ω) |
15 | 1 | ffvelrnda 5507 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐹‘𝑧) ∈
ℕ0) |
16 | 15 | nn0zd 9069 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐹‘𝑧) ∈ ℤ) |
17 | 3 | ffvelrnda 5507 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐺‘𝑧) ∈
ℕ0) |
18 | 17 | nn0zd 9069 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐺‘𝑧) ∈ ℤ) |
19 | | zdceq 9024 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑧) ∈ ℤ ∧ (𝐺‘𝑧) ∈ ℤ) → DECID
(𝐹‘𝑧) = (𝐺‘𝑧)) |
20 | 16, 18, 19 | syl2anc 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
DECID (𝐹‘𝑧) = (𝐺‘𝑧)) |
21 | 12, 14, 20 | ifcldcd 3471 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) ∈
ω) |
22 | 5, 9, 10, 21 | fvmptd3 5466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘𝑧) = if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅)) |
23 | | 1lt2o 6291 |
. . . . . . . . . . . . 13
⊢
1o ∈ 2o |
24 | 23 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
1o ∈ 2o) |
25 | | 0lt2o 6290 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 2o |
26 | 25 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
∅ ∈ 2o) |
27 | 1 | ffvelrnda 5507 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐹‘𝑥) ∈
ℕ0) |
28 | 27 | nn0zd 9069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐹‘𝑥) ∈ ℤ) |
29 | 3 | ffvelrnda 5507 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐺‘𝑥) ∈
ℕ0) |
30 | 29 | nn0zd 9069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐺‘𝑥) ∈ ℤ) |
31 | | zdceq 9024 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℤ ∧ (𝐺‘𝑥) ∈ ℤ) → DECID
(𝐹‘𝑥) = (𝐺‘𝑥)) |
32 | 28, 30, 31 | syl2anc 406 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
DECID (𝐹‘𝑥) = (𝐺‘𝑥)) |
33 | 24, 26, 32 | ifcldcd 3471 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) ∈
2o) |
34 | 33 | fmpttd 5527 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o,
∅)):ℕ∞⟶2o) |
35 | | 2onn 6369 |
. . . . . . . . . . . 12
⊢
2o ∈ ω |
36 | 35 | elexi 2667 |
. . . . . . . . . . 11
⊢
2o ∈ V |
37 | | nninfex 12886 |
. . . . . . . . . . 11
⊢
ℕ∞ ∈ V |
38 | 36, 37 | elmap 6523 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) ∈
(2o ↑𝑚 ℕ∞) ↔
(𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o,
∅)):ℕ∞⟶2o) |
39 | 34, 38 | sylibr 133 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) ∈
(2o ↑𝑚
ℕ∞)) |
40 | | fveq2 5373 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
(𝐹‘𝑥) = (𝐹‘(𝑤 ∈ ω ↦
1o))) |
41 | | fveq2 5373 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
(𝐺‘𝑥) = (𝐺‘(𝑤 ∈ ω ↦
1o))) |
42 | 40, 41 | eqeq12d 2127 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)))) |
43 | 42 | ifbid 3457 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) = if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅)) |
44 | | fconstmpt 4544 |
. . . . . . . . . . . . 13
⊢ (ω
× {1o}) = (𝑤 ∈ ω ↦
1o) |
45 | | infnninf 6970 |
. . . . . . . . . . . . 13
⊢ (ω
× {1o}) ∈ ℕ∞ |
46 | 44, 45 | eqeltrri 2186 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ω ↦
1o) ∈ ℕ∞ |
47 | 46 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ ω ↦ 1o) ∈
ℕ∞) |
48 | | nninffeq.oo |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1o)) =
(𝐺‘(𝑥 ∈ ω ↦
1o))) |
49 | | eqidd 2114 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → 1o =
1o) |
50 | 49 | cbvmptv 3982 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω ↦
1o) = (𝑤 ∈
ω ↦ 1o) |
51 | 50 | fveq2i 5376 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘(𝑥 ∈ ω ↦ 1o)) =
(𝐹‘(𝑤 ∈ ω ↦
1o)) |
52 | 50 | fveq2i 5376 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘(𝑥 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)) |
53 | 48, 51, 52 | 3eqtr3g 2168 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o))) |
54 | 53 | iftrued 3445 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅) = 1o) |
55 | 54, 11 | syl6eqel 2203 |
. . . . . . . . . . 11
⊢ (𝜑 → if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅) ∈ ω) |
56 | 5, 43, 47, 55 | fvmptd3 5466 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑤 ∈ ω ↦
1o)) = if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅)) |
57 | 56, 54 | eqtrd 2145 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑤 ∈ ω ↦
1o)) = 1o) |
58 | | nninffeq.n |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
59 | | fveq2 5373 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → (𝐹‘𝑥) = (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
60 | | fveq2 5373 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → (𝐺‘𝑥) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
61 | 59, 60 | eqeq12d 2127 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o,
∅))))) |
62 | 61 | ifbid 3457 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) = if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅)) |
63 | | nnnninf 6971 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) ∈
ℕ∞) |
64 | 63 | ad2antlr 478 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) ∈
ℕ∞) |
65 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
66 | 65 | iftrued 3445 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅) = 1o) |
67 | 66, 11 | syl6eqel 2203 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅) ∈ ω) |
68 | 5, 62, 64, 67 | fvmptd3 5466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅)) |
69 | 68, 66 | eqtrd 2145 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o) |
70 | 69 | ex 114 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) → ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o)) |
71 | 70 | ralimdva 2471 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) →
∀𝑛 ∈ ω
((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o)) |
72 | 58, 71 | mpd 13 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ω ((𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o) |
73 | 39, 57, 72 | nninfall 12885 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ ℕ∞ ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘𝑧) =
1o) |
74 | 73 | r19.21bi 2492 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘𝑧) =
1o) |
75 | 22, 74 | eqtr3d 2147 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) =
1o) |
76 | 75 | adantr 272 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) =
1o) |
77 | | simpr 109 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → ¬ (𝐹‘𝑧) = (𝐺‘𝑧)) |
78 | 77 | iffalsed 3448 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) =
∅) |
79 | 76, 78 | eqtr3d 2147 |
. . . 4
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → 1o =
∅) |
80 | | 1n0 6281 |
. . . . . 6
⊢
1o ≠ ∅ |
81 | 80 | neii 2282 |
. . . . 5
⊢ ¬
1o = ∅ |
82 | 81 | a1i 9 |
. . . 4
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → ¬ 1o =
∅) |
83 | 79, 82 | pm2.65da 633 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
¬ ¬ (𝐹‘𝑧) = (𝐺‘𝑧)) |
84 | | exmiddc 804 |
. . . 4
⊢
(DECID (𝐹‘𝑧) = (𝐺‘𝑧) → ((𝐹‘𝑧) = (𝐺‘𝑧) ∨ ¬ (𝐹‘𝑧) = (𝐺‘𝑧))) |
85 | 20, 84 | syl 14 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
((𝐹‘𝑧) = (𝐺‘𝑧) ∨ ¬ (𝐹‘𝑧) = (𝐺‘𝑧))) |
86 | 83, 85 | ecased 1308 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐹‘𝑧) = (𝐺‘𝑧)) |
87 | 2, 4, 86 | eqfnfvd 5473 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |