| Step | Hyp | Ref
 | Expression | 
| 1 |   | nninfsel.e | 
. 2
⊢ 𝐸 = (𝑞 ∈ (2o
↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))) | 
| 2 |   | nninfsellemcl 15655 | 
. . . . 5
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑛 ∈ ω) → if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ∈ 2o) | 
| 3 |   | eqid 2196 | 
. . . . 5
⊢ (𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 4 | 2, 3 | fmptd 5716 | 
. . . 4
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → (𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)):ω⟶2o) | 
| 5 |   | 2onn 6579 | 
. . . . . 6
⊢
2o ∈ ω | 
| 6 | 5 | a1i 9 | 
. . . . 5
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → 2o
∈ ω) | 
| 7 |   | omex 4629 | 
. . . . . 6
⊢ ω
∈ V | 
| 8 | 7 | a1i 9 | 
. . . . 5
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → ω ∈
V) | 
| 9 | 6, 8 | elmapd 6721 | 
. . . 4
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → ((𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) ∈ (2o ↑𝑚
ω) ↔ (𝑛 ∈
ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)):ω⟶2o)) | 
| 10 | 4, 9 | mpbird 167 | 
. . 3
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → (𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) ∈ (2o ↑𝑚
ω)) | 
| 11 |   | nninfsellemsuc 15656 | 
. . . . 5
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ⊆ if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 12 |   | peano2 4631 | 
. . . . . 6
⊢ (𝑗 ∈ ω → suc 𝑗 ∈
ω) | 
| 13 |   | nninfsellemcl 15655 | 
. . . . . . 7
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ suc 𝑗 ∈ ω) →
if(∀𝑘 ∈ suc suc
𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ∈ 2o) | 
| 14 | 12, 13 | sylan2 286 | 
. . . . . 6
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ∈ 2o) | 
| 15 |   | suceq 4437 | 
. . . . . . . . 9
⊢ (𝑛 = suc 𝑗 → suc 𝑛 = suc suc 𝑗) | 
| 16 | 15 | raleqdv 2699 | 
. . . . . . . 8
⊢ (𝑛 = suc 𝑗 → (∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o
↔ ∀𝑘 ∈ suc
suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) =
1o)) | 
| 17 | 16 | ifbid 3582 | 
. . . . . . 7
⊢ (𝑛 = suc 𝑗 → if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 18 | 17, 3 | fvmptg 5637 | 
. . . . . 6
⊢ ((suc
𝑗 ∈ ω ∧
if(∀𝑘 ∈ suc suc
𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ∈ 2o) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) = if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 19 | 12, 14, 18 | syl2an2 594 | 
. . . . 5
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) = if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 20 |   | simpr 110 | 
. . . . . 6
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω) | 
| 21 |   | nninfsellemcl 15655 | 
. . . . . 6
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ∈ 2o) | 
| 22 |   | suceq 4437 | 
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → suc 𝑛 = suc 𝑗) | 
| 23 | 22 | raleqdv 2699 | 
. . . . . . . 8
⊢ (𝑛 = 𝑗 → (∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o
↔ ∀𝑘 ∈ suc
𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) =
1o)) | 
| 24 | 23 | ifbid 3582 | 
. . . . . . 7
⊢ (𝑛 = 𝑗 → if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 25 | 24, 3 | fvmptg 5637 | 
. . . . . 6
⊢ ((𝑗 ∈ ω ∧
if(∀𝑘 ∈ suc
𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) ∈ 2o) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗) = if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 26 | 20, 21, 25 | syl2anc 411 | 
. . . . 5
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗) = if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) | 
| 27 | 11, 19, 26 | 3sstr4d 3228 | 
. . . 4
⊢ ((𝑞 ∈ (2o
↑𝑚 ℕ∞) ∧ 𝑗 ∈ ω) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗)) | 
| 28 | 27 | ralrimiva 2570 | 
. . 3
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → ∀𝑗 ∈ ω ((𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗)) | 
| 29 |   | fveq1 5557 | 
. . . . . 6
⊢ (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) → (𝑓‘suc 𝑗) = ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗)) | 
| 30 |   | fveq1 5557 | 
. . . . . 6
⊢ (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) → (𝑓‘𝑗) = ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗)) | 
| 31 | 29, 30 | sseq12d 3214 | 
. . . . 5
⊢ (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗))) | 
| 32 | 31 | ralbidv 2497 | 
. . . 4
⊢ (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗))) | 
| 33 |   | df-nninf 7186 | 
. . . 4
⊢
ℕ∞ = {𝑓 ∈ (2o
↑𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)} | 
| 34 | 32, 33 | elrab2 2923 | 
. . 3
⊢ ((𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) ∈ ℕ∞ ↔ ((𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) ∈ (2o ↑𝑚
ω) ∧ ∀𝑗
∈ ω ((𝑛 ∈
ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))‘𝑗))) | 
| 35 | 10, 28, 34 | sylanbrc 417 | 
. 2
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) → (𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) ∈ ℕ∞) | 
| 36 | 1, 35 | fmpti 5714 | 
1
⊢ 𝐸:(2o
↑𝑚
ℕ∞)⟶ℕ∞ |