Step | Hyp | Ref
| Expression |
1 | | 1n0 6376 |
. . . . 5
⊢
1o ≠ ∅ |
2 | 1 | nesymi 2373 |
. . . 4
⊢ ¬
∅ = 1o |
3 | | simplr 520 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → 𝑝 ∈
ℕ∞) |
4 | | nninff 7061 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
ℕ∞ → 𝑝:ω⟶2o) |
5 | 4 | ffnd 5319 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
ℕ∞ → 𝑝 Fn ω) |
6 | 3, 5 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → 𝑝 Fn ω) |
7 | | nninfall.q |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ∈ (2o
↑𝑚 ℕ∞)) |
8 | 7 | ad2antrr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → 𝑄 ∈ (2o
↑𝑚 ℕ∞)) |
9 | | nninfall.inf |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄‘(𝑥 ∈ ω ↦ 1o)) =
1o) |
10 | 9 | ad2antrr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → (𝑄‘(𝑥 ∈ ω ↦ 1o)) =
1o) |
11 | | nninfall.n |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o) |
12 | 11 | ad2antrr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → ∀𝑛 ∈ ω (𝑄‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) =
1o) |
13 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → (𝑄‘𝑝) = ∅) |
14 | 8, 10, 12, 3, 13 | nninfalllem1 13567 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → ∀𝑛 ∈ ω (𝑝‘𝑛) = 1o) |
15 | | eqeq1 2164 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑝‘𝑛) → (𝑎 = 1o ↔ (𝑝‘𝑛) = 1o)) |
16 | 15 | ralrn 5604 |
. . . . . . . . . . . . . 14
⊢ (𝑝 Fn ω →
(∀𝑎 ∈ ran 𝑝 𝑎 = 1o ↔ ∀𝑛 ∈ ω (𝑝‘𝑛) = 1o)) |
17 | 3, 5, 16 | 3syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → (∀𝑎 ∈ ran 𝑝 𝑎 = 1o ↔ ∀𝑛 ∈ ω (𝑝‘𝑛) = 1o)) |
18 | 14, 17 | mpbird 166 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → ∀𝑎 ∈ ran 𝑝 𝑎 = 1o) |
19 | | peano1 4552 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ ω |
20 | | elex2 2728 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∈ ω → ∃𝑏 𝑏 ∈ ω) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
∃𝑏 𝑏 ∈ ω |
22 | | fdm 5324 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝:ω⟶2o
→ dom 𝑝 =
ω) |
23 | 22 | eleq2d 2227 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝:ω⟶2o
→ (𝑏 ∈ dom 𝑝 ↔ 𝑏 ∈ ω)) |
24 | 23 | exbidv 1805 |
. . . . . . . . . . . . . . 15
⊢ (𝑝:ω⟶2o
→ (∃𝑏 𝑏 ∈ dom 𝑝 ↔ ∃𝑏 𝑏 ∈ ω)) |
25 | 21, 24 | mpbiri 167 |
. . . . . . . . . . . . . 14
⊢ (𝑝:ω⟶2o
→ ∃𝑏 𝑏 ∈ dom 𝑝) |
26 | | dmmrnm 4804 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑏 𝑏 ∈ dom 𝑝 ↔ ∃𝑎 𝑎 ∈ ran 𝑝) |
27 | | eqsnm 3718 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎 𝑎 ∈ ran 𝑝 → (ran 𝑝 = {1o} ↔ ∀𝑎 ∈ ran 𝑝 𝑎 = 1o)) |
28 | 26, 27 | sylbi 120 |
. . . . . . . . . . . . . 14
⊢
(∃𝑏 𝑏 ∈ dom 𝑝 → (ran 𝑝 = {1o} ↔ ∀𝑎 ∈ ran 𝑝 𝑎 = 1o)) |
29 | 25, 28 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝑝:ω⟶2o
→ (ran 𝑝 =
{1o} ↔ ∀𝑎 ∈ ran 𝑝 𝑎 = 1o)) |
30 | 3, 4, 29 | 3syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → (ran 𝑝 = {1o} ↔ ∀𝑎 ∈ ran 𝑝 𝑎 = 1o)) |
31 | 18, 30 | mpbird 166 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → ran 𝑝 = {1o}) |
32 | | eqimss 3182 |
. . . . . . . . . . 11
⊢ (ran
𝑝 = {1o} →
ran 𝑝 ⊆
{1o}) |
33 | 31, 32 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → ran 𝑝 ⊆ {1o}) |
34 | | df-f 5173 |
. . . . . . . . . 10
⊢ (𝑝:ω⟶{1o}
↔ (𝑝 Fn ω ∧
ran 𝑝 ⊆
{1o})) |
35 | 6, 33, 34 | sylanbrc 414 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → 𝑝:ω⟶{1o}) |
36 | | 1onn 6464 |
. . . . . . . . . 10
⊢
1o ∈ ω |
37 | | fconst2g 5681 |
. . . . . . . . . 10
⊢
(1o ∈ ω → (𝑝:ω⟶{1o} ↔ 𝑝 = (ω ×
{1o}))) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑝:ω⟶{1o}
↔ 𝑝 = (ω ×
{1o})) |
39 | 35, 38 | sylib 121 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → 𝑝 = (ω ×
{1o})) |
40 | | fconstmpt 4632 |
. . . . . . . 8
⊢ (ω
× {1o}) = (𝑥 ∈ ω ↦
1o) |
41 | 39, 40 | eqtrdi 2206 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → 𝑝 = (𝑥 ∈ ω ↦
1o)) |
42 | 41 | fveq2d 5471 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → (𝑄‘𝑝) = (𝑄‘(𝑥 ∈ ω ↦
1o))) |
43 | 42, 13, 10 | 3eqtr3d 2198 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ ℕ∞) ∧
(𝑄‘𝑝) = ∅) → ∅ =
1o) |
44 | 43 | ex 114 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℕ∞) →
((𝑄‘𝑝) = ∅ → ∅ =
1o)) |
45 | 2, 44 | mtoi 654 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℕ∞) →
¬ (𝑄‘𝑝) = ∅) |
46 | | elmapi 6612 |
. . . . . . 7
⊢ (𝑄 ∈ (2o
↑𝑚 ℕ∞) → 𝑄:ℕ∞⟶2o) |
47 | 7, 46 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑄:ℕ∞⟶2o) |
48 | 47 | ffvelrnda 5601 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℕ∞) →
(𝑄‘𝑝) ∈ 2o) |
49 | | elpri 3583 |
. . . . . 6
⊢ ((𝑄‘𝑝) ∈ {∅, 1o} →
((𝑄‘𝑝) = ∅ ∨ (𝑄‘𝑝) = 1o)) |
50 | | df2o3 6374 |
. . . . . 6
⊢
2o = {∅, 1o} |
51 | 49, 50 | eleq2s 2252 |
. . . . 5
⊢ ((𝑄‘𝑝) ∈ 2o → ((𝑄‘𝑝) = ∅ ∨ (𝑄‘𝑝) = 1o)) |
52 | 48, 51 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℕ∞) →
((𝑄‘𝑝) = ∅ ∨ (𝑄‘𝑝) = 1o)) |
53 | 52 | orcomd 719 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℕ∞) →
((𝑄‘𝑝) = 1o ∨ (𝑄‘𝑝) = ∅)) |
54 | 45, 53 | ecased 1331 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ℕ∞) →
(𝑄‘𝑝) = 1o) |
55 | 54 | ralrimiva 2530 |
1
⊢ (𝜑 → ∀𝑝 ∈ ℕ∞ (𝑄‘𝑝) = 1o) |