Step | Hyp | Ref
| Expression |
1 | | nninffeq.f |
. . 3
⊢ (𝜑 → 𝐹:ℕ∞⟶ℕ0) |
2 | 1 | ffnd 5346 |
. 2
⊢ (𝜑 → 𝐹 Fn
ℕ∞) |
3 | | nninffeq.g |
. . 3
⊢ (𝜑 → 𝐺:ℕ∞⟶ℕ0) |
4 | 3 | ffnd 5346 |
. 2
⊢ (𝜑 → 𝐺 Fn
ℕ∞) |
5 | | eqid 2170 |
. . . . . . . 8
⊢ (𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) = (𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) |
6 | | fveq2 5494 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
7 | | fveq2 5494 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
8 | 6, 7 | eqeq12d 2185 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘𝑧) = (𝐺‘𝑧))) |
9 | 8 | ifbid 3546 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) = if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅)) |
10 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
𝑧 ∈
ℕ∞) |
11 | | 1onn 6496 |
. . . . . . . . . 10
⊢
1o ∈ ω |
12 | 11 | a1i 9 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
1o ∈ ω) |
13 | | peano1 4576 |
. . . . . . . . . 10
⊢ ∅
∈ ω |
14 | 13 | a1i 9 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
∅ ∈ ω) |
15 | 1 | ffvelrnda 5628 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐹‘𝑧) ∈
ℕ0) |
16 | 15 | nn0zd 9319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐹‘𝑧) ∈ ℤ) |
17 | 3 | ffvelrnda 5628 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐺‘𝑧) ∈
ℕ0) |
18 | 17 | nn0zd 9319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐺‘𝑧) ∈ ℤ) |
19 | | zdceq 9274 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑧) ∈ ℤ ∧ (𝐺‘𝑧) ∈ ℤ) → DECID
(𝐹‘𝑧) = (𝐺‘𝑧)) |
20 | 16, 18, 19 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
DECID (𝐹‘𝑧) = (𝐺‘𝑧)) |
21 | 12, 14, 20 | ifcldcd 3560 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) ∈
ω) |
22 | 5, 9, 10, 21 | fvmptd3 5587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘𝑧) = if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅)) |
23 | | 1lt2o 6418 |
. . . . . . . . . . . . 13
⊢
1o ∈ 2o |
24 | 23 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
1o ∈ 2o) |
25 | | 0lt2o 6417 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 2o |
26 | 25 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
∅ ∈ 2o) |
27 | 1 | ffvelrnda 5628 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐹‘𝑥) ∈
ℕ0) |
28 | 27 | nn0zd 9319 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐹‘𝑥) ∈ ℤ) |
29 | 3 | ffvelrnda 5628 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐺‘𝑥) ∈
ℕ0) |
30 | 29 | nn0zd 9319 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
(𝐺‘𝑥) ∈ ℤ) |
31 | | zdceq 9274 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ ℤ ∧ (𝐺‘𝑥) ∈ ℤ) → DECID
(𝐹‘𝑥) = (𝐺‘𝑥)) |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
DECID (𝐹‘𝑥) = (𝐺‘𝑥)) |
33 | 24, 26, 32 | ifcldcd 3560 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ∞) →
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) ∈
2o) |
34 | 33 | fmpttd 5648 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o,
∅)):ℕ∞⟶2o) |
35 | | 2onn 6497 |
. . . . . . . . . . . 12
⊢
2o ∈ ω |
36 | 35 | elexi 2742 |
. . . . . . . . . . 11
⊢
2o ∈ V |
37 | | nninfex 7094 |
. . . . . . . . . . 11
⊢
ℕ∞ ∈ V |
38 | 36, 37 | elmap 6651 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) ∈
(2o ↑𝑚 ℕ∞) ↔
(𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o,
∅)):ℕ∞⟶2o) |
39 | 34, 38 | sylibr 133 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅)) ∈
(2o ↑𝑚
ℕ∞)) |
40 | | fveq2 5494 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
(𝐹‘𝑥) = (𝐹‘(𝑤 ∈ ω ↦
1o))) |
41 | | fveq2 5494 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
(𝐺‘𝑥) = (𝐺‘(𝑤 ∈ ω ↦
1o))) |
42 | 40, 41 | eqeq12d 2185 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)))) |
43 | 42 | ifbid 3546 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑤 ∈ ω ↦ 1o) →
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) = if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅)) |
44 | | infnninf 7096 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ω ↦
1o) ∈ ℕ∞ |
45 | 44 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ ω ↦ 1o) ∈
ℕ∞) |
46 | | nninffeq.oo |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(𝑥 ∈ ω ↦ 1o)) =
(𝐺‘(𝑥 ∈ ω ↦
1o))) |
47 | | eqidd 2171 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → 1o =
1o) |
48 | 47 | cbvmptv 4083 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω ↦
1o) = (𝑤 ∈
ω ↦ 1o) |
49 | 48 | fveq2i 5497 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘(𝑥 ∈ ω ↦ 1o)) =
(𝐹‘(𝑤 ∈ ω ↦
1o)) |
50 | 48 | fveq2i 5497 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘(𝑥 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)) |
51 | 46, 49, 50 | 3eqtr3g 2226 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o))) |
52 | 51 | iftrued 3532 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅) = 1o) |
53 | 52, 11 | eqeltrdi 2261 |
. . . . . . . . . . 11
⊢ (𝜑 → if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅) ∈ ω) |
54 | 5, 43, 45, 53 | fvmptd3 5587 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑤 ∈ ω ↦
1o)) = if((𝐹‘(𝑤 ∈ ω ↦ 1o)) =
(𝐺‘(𝑤 ∈ ω ↦
1o)), 1o, ∅)) |
55 | 54, 52 | eqtrd 2203 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑤 ∈ ω ↦
1o)) = 1o) |
56 | | nninffeq.n |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
57 | | fveq2 5494 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → (𝐹‘𝑥) = (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
58 | | fveq2 5494 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → (𝐺‘𝑥) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
59 | 57, 58 | eqeq12d 2185 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → ((𝐹‘𝑥) = (𝐺‘𝑥) ↔ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o,
∅))))) |
60 | 59 | ifbid 3546 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) → if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅) = if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅)) |
61 | | nnnninf 7098 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) ∈
ℕ∞) |
62 | 61 | ad2antlr 486 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) ∈
ℕ∞) |
63 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) |
64 | 63 | iftrued 3532 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅) = 1o) |
65 | 64, 11 | eqeltrdi 2261 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅) ∈ ω) |
66 | 5, 60, 62, 65 | fvmptd3 5587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = if((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))), 1o,
∅)) |
67 | 66, 64 | eqtrd 2203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ω) ∧ (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))) → ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o) |
68 | 67 | ex 114 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ω) → ((𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) → ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o)) |
69 | 68 | ralimdva 2537 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑛 ∈ ω (𝐹‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) = (𝐺‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) →
∀𝑛 ∈ ω
((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o)) |
70 | 56, 69 | mpd 13 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑛 ∈ ω ((𝑥 ∈ ℕ∞ ↦
if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o) |
71 | 39, 55, 70 | nninfall 14002 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ ℕ∞ ((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘𝑧) =
1o) |
72 | 71 | r19.21bi 2558 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
((𝑥 ∈
ℕ∞ ↦ if((𝐹‘𝑥) = (𝐺‘𝑥), 1o, ∅))‘𝑧) =
1o) |
73 | 22, 72 | eqtr3d 2205 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) =
1o) |
74 | 73 | adantr 274 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) =
1o) |
75 | | simpr 109 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → ¬ (𝐹‘𝑧) = (𝐺‘𝑧)) |
76 | 75 | iffalsed 3535 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → if((𝐹‘𝑧) = (𝐺‘𝑧), 1o, ∅) =
∅) |
77 | 74, 76 | eqtr3d 2205 |
. . . 4
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → 1o =
∅) |
78 | | 1n0 6408 |
. . . . . 6
⊢
1o ≠ ∅ |
79 | 78 | neii 2342 |
. . . . 5
⊢ ¬
1o = ∅ |
80 | 79 | a1i 9 |
. . . 4
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ∞) ∧
¬ (𝐹‘𝑧) = (𝐺‘𝑧)) → ¬ 1o =
∅) |
81 | 77, 80 | pm2.65da 656 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
¬ ¬ (𝐹‘𝑧) = (𝐺‘𝑧)) |
82 | | exmiddc 831 |
. . . 4
⊢
(DECID (𝐹‘𝑧) = (𝐺‘𝑧) → ((𝐹‘𝑧) = (𝐺‘𝑧) ∨ ¬ (𝐹‘𝑧) = (𝐺‘𝑧))) |
83 | 20, 82 | syl 14 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
((𝐹‘𝑧) = (𝐺‘𝑧) ∨ ¬ (𝐹‘𝑧) = (𝐺‘𝑧))) |
84 | 81, 83 | ecased 1344 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ∞) →
(𝐹‘𝑧) = (𝐺‘𝑧)) |
85 | 2, 4, 84 | eqfnfvd 5594 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |