Step | Hyp | Ref
| Expression |
1 | | 1oex 6314 |
. . . . . . . 8
⊢
1o ∈ V |
2 | 1 | sucid 4334 |
. . . . . . 7
⊢
1o ∈ suc 1o |
3 | | df-2o 6307 |
. . . . . . 7
⊢
2o = suc 1o |
4 | 2, 3 | eleqtrri 2213 |
. . . . . 6
⊢
1o ∈ 2o |
5 | 4 | a1i 9 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) →
1o ∈ 2o) |
6 | | 2on0 6316 |
. . . . . . 7
⊢
2o ≠ ∅ |
7 | | 2onn 6410 |
. . . . . . . 8
⊢
2o ∈ ω |
8 | | nn0eln0 4528 |
. . . . . . . 8
⊢
(2o ∈ ω → (∅ ∈ 2o
↔ 2o ≠ ∅)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢ (∅
∈ 2o ↔ 2o ≠ ∅) |
10 | 6, 9 | mpbir 145 |
. . . . . 6
⊢ ∅
∈ 2o |
11 | 10 | a1i 9 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) → ∅
∈ 2o) |
12 | | nndcel 6389 |
. . . . . 6
⊢ ((𝑖 ∈ ω ∧ 𝑁 ∈ ω) →
DECID 𝑖
∈ 𝑁) |
13 | 12 | ancoms 266 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) →
DECID 𝑖
∈ 𝑁) |
14 | 5, 11, 13 | ifcldcd 3502 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑖 ∈ ω) → if(𝑖 ∈ 𝑁, 1o, ∅) ∈
2o) |
15 | | eqid 2137 |
. . . 4
⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) |
16 | 14, 15 | fmptd 5567 |
. . 3
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o,
∅)):ω⟶2o) |
17 | 7 | elexi 2693 |
. . . 4
⊢
2o ∈ V |
18 | | omex 4502 |
. . . 4
⊢ ω
∈ V |
19 | 17, 18 | elmap 6564 |
. . 3
⊢ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈
(2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o,
∅)):ω⟶2o) |
20 | 16, 19 | sylibr 133 |
. 2
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈
(2o ↑𝑚 ω)) |
21 | | ssid 3112 |
. . . . . . . . 9
⊢
1o ⊆ 1o |
22 | | iftrue 3474 |
. . . . . . . . . . 11
⊢ (suc
𝑗 ∈ 𝑁 → if(suc 𝑗 ∈ 𝑁, 1o, ∅) =
1o) |
23 | 22 | sseq1d 3121 |
. . . . . . . . . 10
⊢ (suc
𝑗 ∈ 𝑁 → (if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o ↔ 1o ⊆ 1o)) |
24 | 23 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ suc 𝑗 ∈ 𝑁) → (if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o ↔ 1o ⊆ 1o)) |
25 | 21, 24 | mpbiri 167 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ suc 𝑗 ∈ 𝑁) → if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o) |
26 | | 0ss 3396 |
. . . . . . . . 9
⊢ ∅
⊆ 1o |
27 | | iffalse 3477 |
. . . . . . . . . . 11
⊢ (¬
suc 𝑗 ∈ 𝑁 → if(suc 𝑗 ∈ 𝑁, 1o, ∅) =
∅) |
28 | 27 | sseq1d 3121 |
. . . . . . . . . 10
⊢ (¬
suc 𝑗 ∈ 𝑁 → (if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o ↔ ∅ ⊆ 1o)) |
29 | 28 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ suc
𝑗 ∈ 𝑁) → (if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o ↔ ∅ ⊆ 1o)) |
30 | 26, 29 | mpbiri 167 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬ suc
𝑗 ∈ 𝑁) → if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o) |
31 | | peano2 4504 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → suc 𝑗 ∈
ω) |
32 | 31 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → suc
𝑗 ∈
ω) |
33 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → 𝑁 ∈
ω) |
34 | | nndcel 6389 |
. . . . . . . . . 10
⊢ ((suc
𝑗 ∈ ω ∧
𝑁 ∈ ω) →
DECID suc 𝑗
∈ 𝑁) |
35 | 32, 33, 34 | syl2anc 408 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) →
DECID suc 𝑗
∈ 𝑁) |
36 | | exmiddc 821 |
. . . . . . . . 9
⊢
(DECID suc 𝑗 ∈ 𝑁 → (suc 𝑗 ∈ 𝑁 ∨ ¬ suc 𝑗 ∈ 𝑁)) |
37 | 35, 36 | syl 14 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (suc
𝑗 ∈ 𝑁 ∨ ¬ suc 𝑗 ∈ 𝑁)) |
38 | 25, 30, 37 | mpjaodan 787 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(suc
𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o) |
39 | 38 | adantr 274 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑗 ∈ 𝑁) → if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆
1o) |
40 | | iftrue 3474 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑁 → if(𝑗 ∈ 𝑁, 1o, ∅) =
1o) |
41 | 40 | adantl 275 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑗 ∈ 𝑁) → if(𝑗 ∈ 𝑁, 1o, ∅) =
1o) |
42 | 39, 41 | sseqtrrd 3131 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑗 ∈ 𝑁) → if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆ if(𝑗 ∈ 𝑁, 1o, ∅)) |
43 | | ssid 3112 |
. . . . . . 7
⊢ ∅
⊆ ∅ |
44 | 43 | a1i 9 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬
𝑗 ∈ 𝑁) → ∅ ⊆
∅) |
45 | | nnord 4520 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ω → Ord 𝑁) |
46 | | ordtr 4295 |
. . . . . . . . . . . 12
⊢ (Ord
𝑁 → Tr 𝑁) |
47 | 45, 46 | syl 14 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω → Tr 𝑁) |
48 | | trsuc 4339 |
. . . . . . . . . . 11
⊢ ((Tr
𝑁 ∧ suc 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
49 | 47, 48 | sylan 281 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧ suc 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
50 | 49 | ex 114 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → (suc
𝑗 ∈ 𝑁 → 𝑗 ∈ 𝑁)) |
51 | 50 | adantr 274 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (suc
𝑗 ∈ 𝑁 → 𝑗 ∈ 𝑁)) |
52 | 51 | con3dimp 624 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬
𝑗 ∈ 𝑁) → ¬ suc 𝑗 ∈ 𝑁) |
53 | 52, 27 | syl 14 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬
𝑗 ∈ 𝑁) → if(suc 𝑗 ∈ 𝑁, 1o, ∅) =
∅) |
54 | | iffalse 3477 |
. . . . . . 7
⊢ (¬
𝑗 ∈ 𝑁 → if(𝑗 ∈ 𝑁, 1o, ∅) =
∅) |
55 | 54 | adantl 275 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬
𝑗 ∈ 𝑁) → if(𝑗 ∈ 𝑁, 1o, ∅) =
∅) |
56 | 44, 53, 55 | 3sstr4d 3137 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ 𝑗 ∈ ω) ∧ ¬
𝑗 ∈ 𝑁) → if(suc 𝑗 ∈ 𝑁, 1o, ∅) ⊆ if(𝑗 ∈ 𝑁, 1o, ∅)) |
57 | | nndcel 6389 |
. . . . . . 7
⊢ ((𝑗 ∈ ω ∧ 𝑁 ∈ ω) →
DECID 𝑗
∈ 𝑁) |
58 | 57 | ancoms 266 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) →
DECID 𝑗
∈ 𝑁) |
59 | | exmiddc 821 |
. . . . . 6
⊢
(DECID 𝑗 ∈ 𝑁 → (𝑗 ∈ 𝑁 ∨ ¬ 𝑗 ∈ 𝑁)) |
60 | 58, 59 | syl 14 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → (𝑗 ∈ 𝑁 ∨ ¬ 𝑗 ∈ 𝑁)) |
61 | 42, 56, 60 | mpjaodan 787 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(suc
𝑗 ∈ 𝑁, 1o, ∅) ⊆ if(𝑗 ∈ 𝑁, 1o, ∅)) |
62 | 4 | a1i 9 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) →
1o ∈ 2o) |
63 | 10 | a1i 9 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ∅
∈ 2o) |
64 | 62, 63, 35 | ifcldcd 3502 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(suc
𝑗 ∈ 𝑁, 1o, ∅) ∈
2o) |
65 | | eleq1 2200 |
. . . . . . 7
⊢ (𝑖 = suc 𝑗 → (𝑖 ∈ 𝑁 ↔ suc 𝑗 ∈ 𝑁)) |
66 | 65 | ifbid 3488 |
. . . . . 6
⊢ (𝑖 = suc 𝑗 → if(𝑖 ∈ 𝑁, 1o, ∅) = if(suc 𝑗 ∈ 𝑁, 1o, ∅)) |
67 | 66, 15 | fvmptg 5490 |
. . . . 5
⊢ ((suc
𝑗 ∈ ω ∧
if(suc 𝑗 ∈ 𝑁, 1o, ∅) ∈
2o) → ((𝑖
∈ ω ↦ if(𝑖
∈ 𝑁, 1o,
∅))‘suc 𝑗) =
if(suc 𝑗 ∈ 𝑁, 1o,
∅)) |
68 | 32, 64, 67 | syl2anc 408 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘suc 𝑗) = if(suc 𝑗 ∈ 𝑁, 1o, ∅)) |
69 | | simpr 109 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → 𝑗 ∈
ω) |
70 | 62, 63, 58 | ifcldcd 3502 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → if(𝑗 ∈ 𝑁, 1o, ∅) ∈
2o) |
71 | | eleq1 2200 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑁 ↔ 𝑗 ∈ 𝑁)) |
72 | 71 | ifbid 3488 |
. . . . . 6
⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑁, 1o, ∅) = if(𝑗 ∈ 𝑁, 1o, ∅)) |
73 | 72, 15 | fvmptg 5490 |
. . . . 5
⊢ ((𝑗 ∈ ω ∧ if(𝑗 ∈ 𝑁, 1o, ∅) ∈
2o) → ((𝑖
∈ ω ↦ if(𝑖
∈ 𝑁, 1o,
∅))‘𝑗) =
if(𝑗 ∈ 𝑁, 1o,
∅)) |
74 | 69, 70, 73 | syl2anc 408 |
. . . 4
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗) = if(𝑗 ∈ 𝑁, 1o, ∅)) |
75 | 61, 68, 74 | 3sstr4d 3137 |
. . 3
⊢ ((𝑁 ∈ ω ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗)) |
76 | 75 | ralrimiva 2503 |
. 2
⊢ (𝑁 ∈ ω →
∀𝑗 ∈ ω
((𝑖 ∈ ω ↦
if(𝑖 ∈ 𝑁, 1o,
∅))‘suc 𝑗)
⊆ ((𝑖 ∈ ω
↦ if(𝑖 ∈ 𝑁, 1o,
∅))‘𝑗)) |
77 | | fveq1 5413 |
. . . . 5
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) → (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘suc 𝑗)) |
78 | | fveq1 5413 |
. . . . 5
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) → (𝑓‘𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗)) |
79 | 77, 78 | sseq12d 3123 |
. . . 4
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗))) |
80 | 79 | ralbidv 2435 |
. . 3
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) →
(∀𝑗 ∈ ω
(𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗))) |
81 | | df-nninf 7000 |
. . 3
⊢
ℕ∞ = {𝑓 ∈ (2o
↑𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)} |
82 | 80, 81 | elrab2 2838 |
. 2
⊢ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈
ℕ∞ ↔ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈
(2o ↑𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))‘𝑗))) |
83 | 20, 76, 82 | sylanbrc 413 |
1
⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈
ℕ∞) |