Proof of Theorem nninfisollemne
Step | Hyp | Ref
| Expression |
1 | | nninfisollemne.0 |
. . . . 5
⊢ (𝜑 → (𝑋‘∪ 𝑁) = ∅) |
2 | 1 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑋‘∪ 𝑁) = ∅) |
3 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) |
4 | 3 | fveq1d 5496 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘∪ 𝑁) =
(𝑋‘∪ 𝑁)) |
5 | | eqid 2170 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) |
6 | | eleq1 2233 |
. . . . . . . . . . 11
⊢ (𝑖 = ∪
𝑁 → (𝑖 ∈ 𝑁 ↔ ∪ 𝑁 ∈ 𝑁)) |
7 | 6 | ifbid 3546 |
. . . . . . . . . 10
⊢ (𝑖 = ∪
𝑁 → if(𝑖 ∈ 𝑁, 1o, ∅) = if(∪ 𝑁
∈ 𝑁, 1o,
∅)) |
8 | | nninfisol.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ω) |
9 | | nnpredcl 4605 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω → ∪ 𝑁
∈ ω) |
10 | 8, 9 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑁
∈ ω) |
11 | | nninfisollemne.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ ∅) |
12 | | nnpredlt 4606 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≠ ∅) → ∪ 𝑁
∈ 𝑁) |
13 | 8, 11, 12 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑁
∈ 𝑁) |
14 | 13 | iftrued 3532 |
. . . . . . . . . . 11
⊢ (𝜑 → if(∪ 𝑁
∈ 𝑁, 1o,
∅) = 1o) |
15 | | 1lt2o 6418 |
. . . . . . . . . . 11
⊢
1o ∈ 2o |
16 | 14, 15 | eqeltrdi 2261 |
. . . . . . . . . 10
⊢ (𝜑 → if(∪ 𝑁
∈ 𝑁, 1o,
∅) ∈ 2o) |
17 | 5, 7, 10, 16 | fvmptd3 5587 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘∪ 𝑁) =
if(∪ 𝑁 ∈ 𝑁, 1o, ∅)) |
18 | 17, 14 | eqtrd 2203 |
. . . . . . . 8
⊢ (𝜑 → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘∪ 𝑁) =
1o) |
19 | 18 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘∪ 𝑁) =
1o) |
20 | 4, 19 | eqtr3d 2205 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑋‘∪ 𝑁) =
1o) |
21 | | 1n0 6408 |
. . . . . 6
⊢
1o ≠ ∅ |
22 | | pm13.181 2422 |
. . . . . 6
⊢ (((𝑋‘∪ 𝑁) =
1o ∧ 1o ≠ ∅) → (𝑋‘∪ 𝑁) ≠ ∅) |
23 | 20, 21, 22 | sylancl 411 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → (𝑋‘∪ 𝑁) ≠ ∅) |
24 | 23 | neneqd 2361 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) → ¬ (𝑋‘∪ 𝑁) =
∅) |
25 | 2, 24 | pm2.65da 656 |
. . 3
⊢ (𝜑 → ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋) |
26 | 25 | olcd 729 |
. 2
⊢ (𝜑 → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)) |
27 | | df-dc 830 |
. 2
⊢
(DECID (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ↔ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋 ∨ ¬ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = 𝑋)) |
28 | 26, 27 | sylibr 133 |
1
⊢ (𝜑 → DECID
(𝑖 ∈ ω ↦
if(𝑖 ∈ 𝑁, 1o, ∅)) =
𝑋) |