Step | Hyp | Ref
| Expression |
1 | | nns.s |
. 2
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦
(𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖)))) |
2 | | 1lt2o 6402 |
. . . . . . 7
⊢
1o ∈ 2o |
3 | 2 | a1i 9 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → 1o ∈
2o) |
4 | | nninff 7079 |
. . . . . . . 8
⊢ (𝑝 ∈
ℕ∞ → 𝑝:ω⟶2o) |
5 | 4 | adantr 274 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → 𝑝:ω⟶2o) |
6 | | nnpredcl 4595 |
. . . . . . . 8
⊢ (𝑖 ∈ ω → ∪ 𝑖
∈ ω) |
7 | 6 | adantl 275 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → ∪ 𝑖
∈ ω) |
8 | 5, 7 | ffvelrnd 5616 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → (𝑝‘∪ 𝑖) ∈
2o) |
9 | | nndceq0 4590 |
. . . . . . 7
⊢ (𝑖 ∈ ω →
DECID 𝑖 =
∅) |
10 | 9 | adantl 275 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → DECID
𝑖 =
∅) |
11 | 3, 8, 10 | ifcldcd 3551 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
∈ 2o) |
12 | | eqid 2164 |
. . . . 5
⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
= (𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖))) |
13 | 11, 12 | fmptd 5634 |
. . . 4
⊢ (𝑝 ∈
ℕ∞ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))):ω⟶2o) |
14 | | 2onn 6481 |
. . . . 5
⊢
2o ∈ ω |
15 | | omex 4565 |
. . . . 5
⊢ ω
∈ V |
16 | | elmapg 6619 |
. . . . 5
⊢
((2o ∈ ω ∧ ω ∈ V) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖))):ω⟶2o)) |
17 | 14, 15, 16 | mp2an 423 |
. . . 4
⊢ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖))):ω⟶2o) |
18 | 13, 17 | sylibr 133 |
. . 3
⊢ (𝑝 ∈
ℕ∞ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω)) |
19 | | 1on 6383 |
. . . . . . . . 9
⊢
1o ∈ On |
20 | 19 | ontrci 4400 |
. . . . . . . 8
⊢ Tr
1o |
21 | 2 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → 1o ∈
2o) |
22 | 4 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → 𝑝:ω⟶2o) |
23 | | peano2 4567 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ω → suc 𝑗 ∈
ω) |
24 | 23 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → suc 𝑗 ∈
ω) |
25 | | nnpredcl 4595 |
. . . . . . . . . . . . 13
⊢ (suc
𝑗 ∈ ω →
∪ suc 𝑗 ∈ ω) |
26 | 24, 25 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ∪ suc 𝑗 ∈ ω) |
27 | 22, 26 | ffvelrnd 5616 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → (𝑝‘∪ suc 𝑗) ∈
2o) |
28 | | nndceq0 4590 |
. . . . . . . . . . . 12
⊢ (suc
𝑗 ∈ ω →
DECID suc 𝑗
= ∅) |
29 | 24, 28 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → DECID
suc 𝑗 =
∅) |
30 | 21, 27, 29 | ifcldcd 3551 |
. . . . . . . . . 10
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ∈ 2o) |
31 | 30 | adantr 274 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ∈ 2o) |
32 | | df-2o 6377 |
. . . . . . . . 9
⊢
2o = suc 1o |
33 | 31, 32 | eleqtrdi 2257 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ∈ suc 1o) |
34 | | trsucss 4396 |
. . . . . . . 8
⊢ (Tr
1o → (if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ∈ suc 1o → if(suc
𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ⊆ 1o)) |
35 | 20, 33, 34 | mpsyl 65 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ⊆ 1o) |
36 | | iftrue 3521 |
. . . . . . . 8
⊢ (𝑗 = ∅ → if(𝑗 = ∅, 1o,
(𝑝‘∪ 𝑗))
= 1o) |
37 | 36 | adantl 275 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))
= 1o) |
38 | 35, 37 | sseqtrrd 3177 |
. . . . . 6
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
39 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω) |
40 | 39 | adantr 274 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ∈
ω) |
41 | | nnord 4584 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → Ord 𝑗) |
42 | | ordtr 4351 |
. . . . . . . . . . 11
⊢ (Ord
𝑗 → Tr 𝑗) |
43 | 40, 41, 42 | 3syl 17 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → Tr 𝑗) |
44 | | unisucg 4387 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → (Tr 𝑗 ↔ ∪ suc 𝑗 = 𝑗)) |
45 | 40, 44 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (Tr 𝑗 ↔ ∪ suc 𝑗 = 𝑗)) |
46 | 43, 45 | mpbid 146 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∪ suc 𝑗 = 𝑗) |
47 | 46 | fveq2d 5485 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘∪ suc 𝑗) = (𝑝‘𝑗)) |
48 | | simpr 109 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ 𝑗 = ∅) |
49 | 48 | neqned 2341 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ≠ ∅) |
50 | | nnsucpred 4589 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → suc ∪ 𝑗 =
𝑗) |
51 | 40, 49, 50 | syl2anc 409 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → suc ∪ 𝑗 =
𝑗) |
52 | 51 | fveq2d 5485 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc ∪ 𝑗) =
(𝑝‘𝑗)) |
53 | | suceq 4375 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∪
𝑗 → suc 𝑘 = suc ∪ 𝑗) |
54 | 53 | fveq2d 5485 |
. . . . . . . . . . 11
⊢ (𝑘 = ∪
𝑗 → (𝑝‘suc 𝑘) = (𝑝‘suc ∪ 𝑗)) |
55 | | fveq2 5481 |
. . . . . . . . . . 11
⊢ (𝑘 = ∪
𝑗 → (𝑝‘𝑘) = (𝑝‘∪ 𝑗)) |
56 | 54, 55 | sseq12d 3169 |
. . . . . . . . . 10
⊢ (𝑘 = ∪
𝑗 → ((𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘) ↔ (𝑝‘suc ∪ 𝑗) ⊆ (𝑝‘∪ 𝑗))) |
57 | | fveq1 5480 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑝 → (𝑓‘suc 𝑗) = (𝑝‘suc 𝑗)) |
58 | | fveq1 5480 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑝 → (𝑓‘𝑗) = (𝑝‘𝑗)) |
59 | 57, 58 | sseq12d 3169 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑝 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗))) |
60 | 59 | ralbidv 2464 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑝 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗))) |
61 | | df-nninf 7077 |
. . . . . . . . . . . . . 14
⊢
ℕ∞ = {𝑓 ∈ (2o
↑𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)} |
62 | 60, 61 | elrab2 2881 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
ℕ∞ ↔ (𝑝 ∈ (2o
↑𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗))) |
63 | 62 | simprbi 273 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
ℕ∞ → ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗)) |
64 | | suceq 4375 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘) |
65 | 64 | fveq2d 5485 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → (𝑝‘suc 𝑗) = (𝑝‘suc 𝑘)) |
66 | | fveq2 5481 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → (𝑝‘𝑗) = (𝑝‘𝑘)) |
67 | 65, 66 | sseq12d 3169 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → ((𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗) ↔ (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘))) |
68 | 67 | cbvralv 2690 |
. . . . . . . . . . . 12
⊢
(∀𝑗 ∈
ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗) ↔ ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘)) |
69 | 63, 68 | sylib 121 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
ℕ∞ → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘)) |
70 | 69 | ad2antrr 480 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘)) |
71 | | nnpredcl 4595 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ω → ∪ 𝑗
∈ ω) |
72 | 71 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ∪ 𝑗
∈ ω) |
73 | 72 | adantr 274 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∪ 𝑗
∈ ω) |
74 | 56, 70, 73 | rspcdva 2831 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc ∪ 𝑗)
⊆ (𝑝‘∪ 𝑗)) |
75 | 52, 74 | eqsstrrd 3175 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘𝑗) ⊆ (𝑝‘∪ 𝑗)) |
76 | 47, 75 | eqsstrd 3174 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘∪ suc 𝑗) ⊆ (𝑝‘∪ 𝑗)) |
77 | | peano3 4568 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ω → suc 𝑗 ≠ ∅) |
78 | 77 | neneqd 2355 |
. . . . . . . . 9
⊢ (𝑗 ∈ ω → ¬ suc
𝑗 =
∅) |
79 | 78 | ad2antlr 481 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ suc
𝑗 =
∅) |
80 | 79 | iffalsed 3526 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) = (𝑝‘∪ suc 𝑗)) |
81 | 48 | iffalsed 3526 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(𝑗 = ∅, 1o,
(𝑝‘∪ 𝑗))
= (𝑝‘∪ 𝑗)) |
82 | 76, 80, 81 | 3sstr4d 3183 |
. . . . . 6
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
83 | | nndceq0 4590 |
. . . . . . . 8
⊢ (𝑗 ∈ ω →
DECID 𝑗 =
∅) |
84 | 83 | adantl 275 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → DECID
𝑗 =
∅) |
85 | | exmiddc 826 |
. . . . . . 7
⊢
(DECID 𝑗 = ∅ → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅)) |
86 | 84, 85 | syl 14 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅)) |
87 | 38, 82, 86 | mpjaodan 788 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
88 | | eqeq1 2171 |
. . . . . . . 8
⊢ (𝑖 = suc 𝑗 → (𝑖 = ∅ ↔ suc 𝑗 = ∅)) |
89 | | unieq 3793 |
. . . . . . . . 9
⊢ (𝑖 = suc 𝑗 → ∪ 𝑖 = ∪
suc 𝑗) |
90 | 89 | fveq2d 5485 |
. . . . . . . 8
⊢ (𝑖 = suc 𝑗 → (𝑝‘∪ 𝑖) = (𝑝‘∪ suc 𝑗)) |
91 | 88, 90 | ifbieq2d 3540 |
. . . . . . 7
⊢ (𝑖 = suc 𝑗 → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
= if(suc 𝑗 = ∅,
1o, (𝑝‘∪ suc 𝑗))) |
92 | 91, 12 | fvmptg 5557 |
. . . . . 6
⊢ ((suc
𝑗 ∈ ω ∧
if(suc 𝑗 = ∅,
1o, (𝑝‘∪ suc 𝑗)) ∈ 2o) →
((𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗))) |
93 | 24, 30, 92 | syl2anc 409 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗))) |
94 | 22, 72 | ffvelrnd 5616 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → (𝑝‘∪ 𝑗) ∈
2o) |
95 | 21, 94, 84 | ifcldcd 3551 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))
∈ 2o) |
96 | | eqeq1 2171 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑖 = ∅ ↔ 𝑗 = ∅)) |
97 | | unieq 3793 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ∪ 𝑖 = ∪
𝑗) |
98 | 97 | fveq2d 5485 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑝‘∪ 𝑖) = (𝑝‘∪ 𝑗)) |
99 | 96, 98 | ifbieq2d 3540 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
= if(𝑗 = ∅,
1o, (𝑝‘∪ 𝑗))) |
100 | 99, 12 | fvmptg 5557 |
. . . . . 6
⊢ ((𝑗 ∈ ω ∧ if(𝑗 = ∅, 1o,
(𝑝‘∪ 𝑗))
∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗) = if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
101 | 39, 95, 100 | syl2anc 409 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗) = if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
102 | 87, 93, 101 | 3sstr4d 3183 |
. . . 4
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗)) |
103 | 102 | ralrimiva 2537 |
. . 3
⊢ (𝑝 ∈
ℕ∞ → ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗)) |
104 | | fveq1 5480 |
. . . . . 6
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗)) |
105 | | fveq1 5480 |
. . . . . 6
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ (𝑓‘𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗)) |
106 | 104, 105 | sseq12d 3169 |
. . . . 5
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗))) |
107 | 106 | ralbidv 2464 |
. . . 4
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ (∀𝑗 ∈
ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗))) |
108 | 107, 61 | elrab2 2881 |
. . 3
⊢ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
∈ ℕ∞ ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗))) |
109 | 18, 103, 108 | sylanbrc 414 |
. 2
⊢ (𝑝 ∈
ℕ∞ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
∈ ℕ∞) |
110 | 1, 109 | fmpti 5632 |
1
⊢ 𝑆:ℕ∞⟶ℕ∞ |