Proof of Theorem peano3nninf
Step | Hyp | Ref
| Expression |
1 | | fveq1 5420 |
. . . . . . . . . 10
⊢ (𝑝 = 𝐴 → (𝑝‘∪ 𝑖) = (𝐴‘∪ 𝑖)) |
2 | 1 | ifeq2d 3490 |
. . . . . . . . 9
⊢ (𝑝 = 𝐴 → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
= if(𝑖 = ∅,
1o, (𝐴‘∪ 𝑖))) |
3 | 2 | mpteq2dv 4019 |
. . . . . . . 8
⊢ (𝑝 = 𝐴 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
= (𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝐴‘∪ 𝑖)))) |
4 | | peano3nninf.s |
. . . . . . . 8
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦
(𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖)))) |
5 | | omex 4507 |
. . . . . . . . 9
⊢ ω
∈ V |
6 | 5 | mptex 5646 |
. . . . . . . 8
⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝐴‘∪ 𝑖)))
∈ V |
7 | 3, 4, 6 | fvmpt 5498 |
. . . . . . 7
⊢ (𝐴 ∈
ℕ∞ → (𝑆‘𝐴) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝐴‘∪ 𝑖)))) |
8 | | eqeq1 2146 |
. . . . . . . . 9
⊢ (𝑖 = ∅ → (𝑖 = ∅ ↔ ∅ =
∅)) |
9 | | unieq 3745 |
. . . . . . . . . 10
⊢ (𝑖 = ∅ → ∪ 𝑖 =
∪ ∅) |
10 | 9 | fveq2d 5425 |
. . . . . . . . 9
⊢ (𝑖 = ∅ → (𝐴‘∪ 𝑖) =
(𝐴‘∪ ∅)) |
11 | 8, 10 | ifbieq2d 3496 |
. . . . . . . 8
⊢ (𝑖 = ∅ → if(𝑖 = ∅, 1o,
(𝐴‘∪ 𝑖))
= if(∅ = ∅, 1o, (𝐴‘∪
∅))) |
12 | 11 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ∈
ℕ∞ ∧ 𝑖 = ∅) → if(𝑖 = ∅, 1o, (𝐴‘∪ 𝑖)) = if(∅ = ∅,
1o, (𝐴‘∪
∅))) |
13 | | peano1 4508 |
. . . . . . . 8
⊢ ∅
∈ ω |
14 | 13 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈
ℕ∞ → ∅ ∈ ω) |
15 | | eqid 2139 |
. . . . . . . . . 10
⊢ ∅ =
∅ |
16 | 15 | iftruei 3480 |
. . . . . . . . 9
⊢
if(∅ = ∅, 1o, (𝐴‘∪
∅)) = 1o |
17 | | 1onn 6416 |
. . . . . . . . 9
⊢
1o ∈ ω |
18 | 16, 17 | eqeltri 2212 |
. . . . . . . 8
⊢
if(∅ = ∅, 1o, (𝐴‘∪
∅)) ∈ ω |
19 | 18 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈
ℕ∞ → if(∅ = ∅, 1o, (𝐴‘∪ ∅)) ∈ ω) |
20 | 7, 12, 14, 19 | fvmptd 5502 |
. . . . . 6
⊢ (𝐴 ∈
ℕ∞ → ((𝑆‘𝐴)‘∅) = if(∅ = ∅,
1o, (𝐴‘∪
∅))) |
21 | 20, 16 | syl6eq 2188 |
. . . . 5
⊢ (𝐴 ∈
ℕ∞ → ((𝑆‘𝐴)‘∅) =
1o) |
22 | 21 | adantr 274 |
. . . 4
⊢ ((𝐴 ∈
ℕ∞ ∧ (𝑆‘𝐴) = (𝑥 ∈ ω ↦ ∅)) →
((𝑆‘𝐴)‘∅) =
1o) |
23 | | fveq1 5420 |
. . . . . 6
⊢ ((𝑆‘𝐴) = (𝑥 ∈ ω ↦ ∅) →
((𝑆‘𝐴)‘∅) = ((𝑥 ∈ ω ↦
∅)‘∅)) |
24 | 23 | adantl 275 |
. . . . 5
⊢ ((𝐴 ∈
ℕ∞ ∧ (𝑆‘𝐴) = (𝑥 ∈ ω ↦ ∅)) →
((𝑆‘𝐴)‘∅) = ((𝑥 ∈ ω ↦
∅)‘∅)) |
25 | 15 | a1i 9 |
. . . . . . 7
⊢ (𝑥 = ∅ → ∅ =
∅) |
26 | | eqid 2139 |
. . . . . . 7
⊢ (𝑥 ∈ ω ↦ ∅)
= (𝑥 ∈ ω ↦
∅) |
27 | 25, 26 | fvmptg 5497 |
. . . . . 6
⊢ ((∅
∈ ω ∧ ∅ ∈ ω) → ((𝑥 ∈ ω ↦
∅)‘∅) = ∅) |
28 | 13, 13, 27 | mp2an 422 |
. . . . 5
⊢ ((𝑥 ∈ ω ↦
∅)‘∅) = ∅ |
29 | 24, 28 | syl6eq 2188 |
. . . 4
⊢ ((𝐴 ∈
ℕ∞ ∧ (𝑆‘𝐴) = (𝑥 ∈ ω ↦ ∅)) →
((𝑆‘𝐴)‘∅) = ∅) |
30 | 22, 29 | eqtr3d 2174 |
. . 3
⊢ ((𝐴 ∈
ℕ∞ ∧ (𝑆‘𝐴) = (𝑥 ∈ ω ↦ ∅)) →
1o = ∅) |
31 | | 1n0 6329 |
. . . . 5
⊢
1o ≠ ∅ |
32 | 31 | neii 2310 |
. . . 4
⊢ ¬
1o = ∅ |
33 | 32 | a1i 9 |
. . 3
⊢ ((𝐴 ∈
ℕ∞ ∧ (𝑆‘𝐴) = (𝑥 ∈ ω ↦ ∅)) →
¬ 1o = ∅) |
34 | 30, 33 | pm2.65da 650 |
. 2
⊢ (𝐴 ∈
ℕ∞ → ¬ (𝑆‘𝐴) = (𝑥 ∈ ω ↦
∅)) |
35 | 34 | neqned 2315 |
1
⊢ (𝐴 ∈
ℕ∞ → (𝑆‘𝐴) ≠ (𝑥 ∈ ω ↦
∅)) |