Step | Hyp | Ref
| Expression |
1 | | elequ1 1654 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑖 → (𝑐 ∈ 𝑏 ↔ 𝑖 ∈ 𝑏)) |
2 | 1 | ifbid 3432 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑖 → if(𝑐 ∈ 𝑏, 1o, ∅) = if(𝑖 ∈ 𝑏, 1o, ∅)) |
3 | 2 | cbvmptv 3956 |
. . . . . . . . 9
⊢ (𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅)) |
4 | 3 | fveq2i 5343 |
. . . . . . . 8
⊢ (𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = (𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) |
5 | 4 | eqeq1i 2102 |
. . . . . . 7
⊢ ((𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o
↔ (𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) =
1o) |
6 | 5 | ralbii 2395 |
. . . . . 6
⊢
(∀𝑏 ∈
suc 𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o
↔ ∀𝑏 ∈ suc
𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) =
1o) |
7 | | ifbi 3431 |
. . . . . 6
⊢
((∀𝑏 ∈
suc 𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o
↔ ∀𝑏 ∈ suc
𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o)
→ if(∀𝑏 ∈
suc 𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑏 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅)) |
8 | 6, 7 | ax-mp 7 |
. . . . 5
⊢
if(∀𝑏 ∈
suc 𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑏 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅) |
9 | 8 | mpteq2i 3947 |
. . . 4
⊢ (𝑎 ∈ ω ↦
if(∀𝑏 ∈ suc
𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅)) = (𝑎 ∈ ω ↦ if(∀𝑏 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅)) |
10 | | elequ2 1655 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑏 → (𝑖 ∈ 𝑘 ↔ 𝑖 ∈ 𝑏)) |
11 | 10 | ifbid 3432 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑏 → if(𝑖 ∈ 𝑘, 1o, ∅) = if(𝑖 ∈ 𝑏, 1o, ∅)) |
12 | 11 | mpteq2dv 3951 |
. . . . . . . . 9
⊢ (𝑘 = 𝑏 → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) |
13 | 12 | fveq2d 5344 |
. . . . . . . 8
⊢ (𝑘 = 𝑏 → (𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = (𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅)))) |
14 | 13 | eqeq1d 2103 |
. . . . . . 7
⊢ (𝑘 = 𝑏 → ((𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o
↔ (𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) =
1o)) |
15 | 14 | cbvralv 2604 |
. . . . . 6
⊢
(∀𝑘 ∈
suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o
↔ ∀𝑏 ∈ suc
𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) =
1o) |
16 | | ifbi 3431 |
. . . . . 6
⊢
((∀𝑘 ∈
suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o
↔ ∀𝑏 ∈ suc
𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o)
→ if(∀𝑘 ∈
suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑏 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅)) |
17 | 15, 16 | ax-mp 7 |
. . . . 5
⊢
if(∀𝑘 ∈
suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑏 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅) |
18 | 17 | mpteq2i 3947 |
. . . 4
⊢ (𝑎 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) = (𝑎 ∈ ω ↦ if(∀𝑏 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅)) |
19 | | suceq 4253 |
. . . . . . 7
⊢ (𝑎 = 𝑛 → suc 𝑎 = suc 𝑛) |
20 | 19 | raleqdv 2582 |
. . . . . 6
⊢ (𝑎 = 𝑛 → (∀𝑘 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o
↔ ∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) =
1o)) |
21 | 20 | ifbid 3432 |
. . . . 5
⊢ (𝑎 = 𝑛 → if(∀𝑘 ∈ suc 𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅) = if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) |
22 | 21 | cbvmptv 3956 |
. . . 4
⊢ (𝑎 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑎(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) |
23 | 9, 18, 22 | 3eqtr2i 2121 |
. . 3
⊢ (𝑎 ∈ ω ↦
if(∀𝑏 ∈ suc
𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅)) = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅)) |
24 | 23 | mpteq2i 3947 |
. 2
⊢ (𝑞 ∈ (2o
↑𝑚 ℕ∞) ↦ (𝑎 ∈ ω ↦
if(∀𝑏 ∈ suc
𝑎(𝑞‘(𝑐 ∈ ω ↦ if(𝑐 ∈ 𝑏, 1o, ∅))) = 1o,
1o, ∅))) = (𝑞 ∈ (2o
↑𝑚 ℕ∞) ↦ (𝑛 ∈ ω ↦
if(∀𝑘 ∈ suc
𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑘, 1o, ∅))) = 1o,
1o, ∅))) |
25 | 24 | nninfomnilem 12631 |
1
⊢
ℕ∞ ∈ Omni |