Proof of Theorem axlowdimlem7
Step | Hyp | Ref
| Expression |
1 | | axlowdimlem7.1 |
. 2
⊢ 𝑃 = ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) |
2 | | eqid 2610 |
. . . . . . . 8
⊢ {〈3,
-1〉} = {〈3, -1〉} |
3 | | 3ex 10973 |
. . . . . . . . 9
⊢ 3 ∈
V |
4 | | negex 10158 |
. . . . . . . . 9
⊢ -1 ∈
V |
5 | 3, 4 | fsn 6308 |
. . . . . . . 8
⊢
({〈3, -1〉}:{3}⟶{-1} ↔ {〈3, -1〉} =
{〈3, -1〉}) |
6 | 2, 5 | mpbir 220 |
. . . . . . 7
⊢ {〈3,
-1〉}:{3}⟶{-1} |
7 | | neg1rr 11002 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
8 | | snssi 4280 |
. . . . . . . 8
⊢ (-1
∈ ℝ → {-1} ⊆ ℝ) |
9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢ {-1}
⊆ ℝ |
10 | | fss 5969 |
. . . . . . 7
⊢
(({〈3, -1〉}:{3}⟶{-1} ∧ {-1} ⊆ ℝ) →
{〈3, -1〉}:{3}⟶ℝ) |
11 | 6, 9, 10 | mp2an 704 |
. . . . . 6
⊢ {〈3,
-1〉}:{3}⟶ℝ |
12 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
13 | 12 | fconst6 6008 |
. . . . . 6
⊢
(((1...𝑁) ∖
{3}) × {0}):((1...𝑁)
∖ {3})⟶ℝ |
14 | 11, 13 | pm3.2i 470 |
. . . . 5
⊢
({〈3, -1〉}:{3}⟶ℝ ∧ (((1...𝑁) ∖ {3}) × {0}):((1...𝑁) ∖
{3})⟶ℝ) |
15 | | disjdif 3992 |
. . . . 5
⊢ ({3}
∩ ((1...𝑁) ∖
{3})) = ∅ |
16 | | fun2 5980 |
. . . . 5
⊢
((({〈3, -1〉}:{3}⟶ℝ ∧ (((1...𝑁) ∖ {3}) × {0}):((1...𝑁) ∖ {3})⟶ℝ)
∧ ({3} ∩ ((1...𝑁)
∖ {3})) = ∅) → ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0})):({3} ∪ ((1...𝑁)
∖ {3}))⟶ℝ) |
17 | 14, 15, 16 | mp2an 704 |
. . . 4
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})):({3} ∪
((1...𝑁) ∖
{3}))⟶ℝ |
18 | | eluzle 11576 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
19 | | 1le3 11121 |
. . . . . . . . 9
⊢ 1 ≤
3 |
20 | 18, 19 | jctil 558 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 ≤ 3 ∧ 3 ≤ 𝑁)) |
21 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
22 | | 3z 11287 |
. . . . . . . . . 10
⊢ 3 ∈
ℤ |
23 | | 1z 11284 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
24 | | elfz 12203 |
. . . . . . . . . 10
⊢ ((3
∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (3 ∈ (1...𝑁) ↔ (1 ≤ 3 ∧ 3 ≤
𝑁))) |
25 | 22, 23, 24 | mp3an12 1406 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → (3 ∈
(1...𝑁) ↔ (1 ≤ 3
∧ 3 ≤ 𝑁))) |
26 | 21, 25 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → (3 ∈ (1...𝑁) ↔ (1 ≤ 3 ∧ 3 ≤ 𝑁))) |
27 | 20, 26 | mpbird 246 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ∈ (1...𝑁)) |
28 | 27 | snssd 4281 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → {3} ⊆ (1...𝑁)) |
29 | | undif 4001 |
. . . . . 6
⊢ ({3}
⊆ (1...𝑁) ↔ ({3}
∪ ((1...𝑁) ∖
{3})) = (1...𝑁)) |
30 | 28, 29 | sylib 207 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → ({3} ∪ ((1...𝑁) ∖ {3})) = (1...𝑁)) |
31 | 30 | feq2d 5944 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → (({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})):({3} ∪ ((1...𝑁) ∖ {3}))⟶ℝ ↔
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})):(1...𝑁)⟶ℝ)) |
32 | 17, 31 | mpbii 222 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0})):(1...𝑁)⟶ℝ) |
33 | | eluzge3nn 11606 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
34 | | elee 25574 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
(𝔼‘𝑁) ↔
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})):(1...𝑁)⟶ℝ)) |
35 | 33, 34 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → (({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) ∈ (𝔼‘𝑁) ↔ ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})):(1...𝑁)⟶ℝ)) |
36 | 32, 35 | mpbird 246 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0}))
∈ (𝔼‘𝑁)) |
37 | 1, 36 | syl5eqel 2692 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑃 ∈ (𝔼‘𝑁)) |