| Step | Hyp | Ref
| Expression |
| 1 | | nns.s |
. 2
⊢ 𝑆 = (𝑝 ∈ ℕ∞ ↦
(𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖)))) |
| 2 | | 1lt2o 6500 |
. . . . . . 7
⊢
1o ∈ 2o |
| 3 | 2 | a1i 9 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → 1o ∈
2o) |
| 4 | | nninff 7188 |
. . . . . . . 8
⊢ (𝑝 ∈
ℕ∞ → 𝑝:ω⟶2o) |
| 5 | 4 | adantr 276 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → 𝑝:ω⟶2o) |
| 6 | | nnpredcl 4659 |
. . . . . . . 8
⊢ (𝑖 ∈ ω → ∪ 𝑖
∈ ω) |
| 7 | 6 | adantl 277 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → ∪ 𝑖
∈ ω) |
| 8 | 5, 7 | ffvelcdmd 5698 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → (𝑝‘∪ 𝑖) ∈
2o) |
| 9 | | nndceq0 4654 |
. . . . . . 7
⊢ (𝑖 ∈ ω →
DECID 𝑖 =
∅) |
| 10 | 9 | adantl 277 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → DECID
𝑖 =
∅) |
| 11 | 3, 8, 10 | ifcldcd 3597 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑖 ∈ ω) → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
∈ 2o) |
| 12 | | eqid 2196 |
. . . . 5
⊢ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
= (𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖))) |
| 13 | 11, 12 | fmptd 5716 |
. . . 4
⊢ (𝑝 ∈
ℕ∞ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))):ω⟶2o) |
| 14 | | 2onn 6579 |
. . . . 5
⊢
2o ∈ ω |
| 15 | | omex 4629 |
. . . . 5
⊢ ω
∈ V |
| 16 | | elmapg 6720 |
. . . . 5
⊢
((2o ∈ ω ∧ ω ∈ V) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖))):ω⟶2o)) |
| 17 | 14, 15, 16 | mp2an 426 |
. . . 4
⊢ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖))):ω⟶2o) |
| 18 | 13, 17 | sylibr 134 |
. . 3
⊢ (𝑝 ∈
ℕ∞ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω)) |
| 19 | | 1on 6481 |
. . . . . . . . 9
⊢
1o ∈ On |
| 20 | 19 | ontrci 4462 |
. . . . . . . 8
⊢ Tr
1o |
| 21 | 2 | a1i 9 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → 1o ∈
2o) |
| 22 | 4 | adantr 276 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → 𝑝:ω⟶2o) |
| 23 | | peano2 4631 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ω → suc 𝑗 ∈
ω) |
| 24 | 23 | adantl 277 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → suc 𝑗 ∈
ω) |
| 25 | | nnpredcl 4659 |
. . . . . . . . . . . . 13
⊢ (suc
𝑗 ∈ ω →
∪ suc 𝑗 ∈ ω) |
| 26 | 24, 25 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ∪ suc 𝑗 ∈ ω) |
| 27 | 22, 26 | ffvelcdmd 5698 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → (𝑝‘∪ suc 𝑗) ∈
2o) |
| 28 | | nndceq0 4654 |
. . . . . . . . . . . 12
⊢ (suc
𝑗 ∈ ω →
DECID suc 𝑗
= ∅) |
| 29 | 24, 28 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → DECID
suc 𝑗 =
∅) |
| 30 | 21, 27, 29 | ifcldcd 3597 |
. . . . . . . . . 10
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ∈ 2o) |
| 31 | 30 | adantr 276 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ∈ 2o) |
| 32 | | df-2o 6475 |
. . . . . . . . 9
⊢
2o = suc 1o |
| 33 | 31, 32 | eleqtrdi 2289 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ∈ suc 1o) |
| 34 | | trsucss 4458 |
. . . . . . . 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 3566 |
. . . . . . . 8
⊢ (𝑗 = ∅ → if(𝑗 = ∅, 1o,
(𝑝‘∪ 𝑗))
= 1o) |
| 37 | 36 | adantl 277 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))
= 1o) |
| 38 | 35, 37 | sseqtrrd 3222 |
. . . . . 6
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
| 39 | | simpr 110 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω) |
| 40 | 39 | adantr 276 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ∈
ω) |
| 41 | | nnord 4648 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → Ord 𝑗) |
| 42 | | ordtr 4413 |
. . . . . . . . . . 11
⊢ (Ord
𝑗 → Tr 𝑗) |
| 43 | 40, 41, 42 | 3syl 17 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → Tr 𝑗) |
| 44 | | unisucg 4449 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ω → (Tr 𝑗 ↔ ∪ suc 𝑗 = 𝑗)) |
| 45 | 40, 44 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (Tr 𝑗 ↔ ∪ suc 𝑗 = 𝑗)) |
| 46 | 43, 45 | mpbid 147 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∪ suc 𝑗 = 𝑗) |
| 47 | 46 | fveq2d 5562 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘∪ suc 𝑗) = (𝑝‘𝑗)) |
| 48 | | simpr 110 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ 𝑗 = ∅) |
| 49 | 48 | neqned 2374 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ≠ ∅) |
| 50 | | nnsucpred 4653 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → suc ∪ 𝑗 =
𝑗) |
| 51 | 40, 49, 50 | syl2anc 411 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → suc ∪ 𝑗 =
𝑗) |
| 52 | 51 | fveq2d 5562 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc ∪ 𝑗) =
(𝑝‘𝑗)) |
| 53 | | suceq 4437 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∪
𝑗 → suc 𝑘 = suc ∪ 𝑗) |
| 54 | 53 | fveq2d 5562 |
. . . . . . . . . . 11
⊢ (𝑘 = ∪
𝑗 → (𝑝‘suc 𝑘) = (𝑝‘suc ∪ 𝑗)) |
| 55 | | fveq2 5558 |
. . . . . . . . . . 11
⊢ (𝑘 = ∪
𝑗 → (𝑝‘𝑘) = (𝑝‘∪ 𝑗)) |
| 56 | 54, 55 | sseq12d 3214 |
. . . . . . . . . 10
⊢ (𝑘 = ∪
𝑗 → ((𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘) ↔ (𝑝‘suc ∪ 𝑗) ⊆ (𝑝‘∪ 𝑗))) |
| 57 | | fveq1 5557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑝 → (𝑓‘suc 𝑗) = (𝑝‘suc 𝑗)) |
| 58 | | fveq1 5557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑝 → (𝑓‘𝑗) = (𝑝‘𝑗)) |
| 59 | 57, 58 | sseq12d 3214 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑝 → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗))) |
| 60 | 59 | ralbidv 2497 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑝 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗))) |
| 61 | | df-nninf 7186 |
. . . . . . . . . . . . . 14
⊢
ℕ∞ = {𝑓 ∈ (2o
↑𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)} |
| 62 | 60, 61 | elrab2 2923 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
ℕ∞ ↔ (𝑝 ∈ (2o
↑𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗))) |
| 63 | 62 | simprbi 275 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
ℕ∞ → ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗)) |
| 64 | | suceq 4437 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘) |
| 65 | 64 | fveq2d 5562 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → (𝑝‘suc 𝑗) = (𝑝‘suc 𝑘)) |
| 66 | | fveq2 5558 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → (𝑝‘𝑗) = (𝑝‘𝑘)) |
| 67 | 65, 66 | sseq12d 3214 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → ((𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗) ↔ (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘))) |
| 68 | 67 | cbvralv 2729 |
. . . . . . . . . . . 12
⊢
(∀𝑗 ∈
ω (𝑝‘suc 𝑗) ⊆ (𝑝‘𝑗) ↔ ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘)) |
| 69 | 63, 68 | sylib 122 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
ℕ∞ → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘)) |
| 70 | 69 | ad2antrr 488 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝‘𝑘)) |
| 71 | | nnpredcl 4659 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ω → ∪ 𝑗
∈ ω) |
| 72 | 71 | adantl 277 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ∪ 𝑗
∈ ω) |
| 73 | 72 | adantr 276 |
. . . . . . . . . 10
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∪ 𝑗
∈ ω) |
| 74 | 56, 70, 73 | rspcdva 2873 |
. . . . . . . . 9
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc ∪ 𝑗)
⊆ (𝑝‘∪ 𝑗)) |
| 75 | 52, 74 | eqsstrrd 3220 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘𝑗) ⊆ (𝑝‘∪ 𝑗)) |
| 76 | 47, 75 | eqsstrd 3219 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘∪ suc 𝑗) ⊆ (𝑝‘∪ 𝑗)) |
| 77 | | peano3 4632 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ω → suc 𝑗 ≠ ∅) |
| 78 | 77 | neneqd 2388 |
. . . . . . . . 9
⊢ (𝑗 ∈ ω → ¬ suc
𝑗 =
∅) |
| 79 | 78 | ad2antlr 489 |
. . . . . . . 8
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ suc
𝑗 =
∅) |
| 80 | 79 | iffalsed 3571 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) = (𝑝‘∪ suc 𝑗)) |
| 81 | 48 | iffalsed 3571 |
. . . . . . 7
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(𝑗 = ∅, 1o,
(𝑝‘∪ 𝑗))
= (𝑝‘∪ 𝑗)) |
| 82 | 76, 80, 81 | 3sstr4d 3228 |
. . . . . 6
⊢ (((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
| 83 | | nndceq0 4654 |
. . . . . . . 8
⊢ (𝑗 ∈ ω →
DECID 𝑗 =
∅) |
| 84 | 83 | adantl 277 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → DECID
𝑗 =
∅) |
| 85 | | exmiddc 837 |
. . . . . . 7
⊢
(DECID 𝑗 = ∅ → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅)) |
| 86 | 84, 85 | syl 14 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅)) |
| 87 | 38, 82, 86 | mpjaodan 799 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1o,
(𝑝‘∪ suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
| 88 | | eqeq1 2203 |
. . . . . . . 8
⊢ (𝑖 = suc 𝑗 → (𝑖 = ∅ ↔ suc 𝑗 = ∅)) |
| 89 | | unieq 3848 |
. . . . . . . . 9
⊢ (𝑖 = suc 𝑗 → ∪ 𝑖 = ∪
suc 𝑗) |
| 90 | 89 | fveq2d 5562 |
. . . . . . . 8
⊢ (𝑖 = suc 𝑗 → (𝑝‘∪ 𝑖) = (𝑝‘∪ suc 𝑗)) |
| 91 | 88, 90 | ifbieq2d 3585 |
. . . . . . 7
⊢ (𝑖 = suc 𝑗 → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
= if(suc 𝑗 = ∅,
1o, (𝑝‘∪ suc 𝑗))) |
| 92 | 91, 12 | fvmptg 5637 |
. . . . . 6
⊢ ((suc
𝑗 ∈ ω ∧
if(suc 𝑗 = ∅,
1o, (𝑝‘∪ suc 𝑗)) ∈ 2o) →
((𝑖 ∈ ω ↦
if(𝑖 = ∅,
1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗))) |
| 93 | 24, 30, 92 | syl2anc 411 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1o, (𝑝‘∪ suc 𝑗))) |
| 94 | 22, 72 | ffvelcdmd 5698 |
. . . . . . 7
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → (𝑝‘∪ 𝑗) ∈
2o) |
| 95 | 21, 94, 84 | ifcldcd 3597 |
. . . . . 6
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))
∈ 2o) |
| 96 | | eqeq1 2203 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑖 = ∅ ↔ 𝑗 = ∅)) |
| 97 | | unieq 3848 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ∪ 𝑖 = ∪
𝑗) |
| 98 | 97 | fveq2d 5562 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑝‘∪ 𝑖) = (𝑝‘∪ 𝑗)) |
| 99 | 96, 98 | ifbieq2d 3585 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖))
= if(𝑗 = ∅,
1o, (𝑝‘∪ 𝑗))) |
| 100 | 99, 12 | fvmptg 5637 |
. . . . . 6
⊢ ((𝑗 ∈ ω ∧ if(𝑗 = ∅, 1o,
(𝑝‘∪ 𝑗))
∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗) = if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
| 101 | 39, 95, 100 | syl2anc 411 |
. . . . 5
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗) = if(𝑗 = ∅, 1o, (𝑝‘∪ 𝑗))) |
| 102 | 87, 93, 101 | 3sstr4d 3228 |
. . . 4
⊢ ((𝑝 ∈
ℕ∞ ∧ 𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗)) |
| 103 | 102 | ralrimiva 2570 |
. . 3
⊢ (𝑝 ∈
ℕ∞ → ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗)) |
| 104 | | fveq1 5557 |
. . . . . 6
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗)) |
| 105 | | fveq1 5557 |
. . . . . 6
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ (𝑓‘𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗)) |
| 106 | 104, 105 | sseq12d 3214 |
. . . . 5
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗))) |
| 107 | 106 | ralbidv 2497 |
. . . 4
⊢ (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
→ (∀𝑗 ∈
ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗))) |
| 108 | 107, 61 | elrab2 2923 |
. . 3
⊢ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))
∈ ℕ∞ ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
∈ (2o ↑𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o,
(𝑝‘∪ 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))‘𝑗))) |
| 109 | 18, 103, 108 | sylanbrc 417 |
. 2
⊢ (𝑝 ∈
ℕ∞ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝‘∪ 𝑖)))
∈ ℕ∞) |
| 110 | 1, 109 | fmpti 5714 |
1
⊢ 𝑆:ℕ∞⟶ℕ∞ |