Step | Hyp | Ref
| Expression |
1 | | infxpenc2.1 |
. 2
⊢ (𝜑 → 𝐴 ∈ On) |
2 | | infxpenc2.2 |
. 2
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
3 | | infxpenc2.3 |
. 2
⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) |
4 | | infxpenc2.4 |
. 2
⊢ (𝜑 → 𝐹:(ω ↑𝑜
2𝑜)–1-1-onto→ω) |
5 | | infxpenc2.5 |
. 2
⊢ (𝜑 → (𝐹‘∅) = ∅) |
6 | | eqid 2610 |
. 2
⊢ (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜
2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) = (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜
2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) |
7 | | eqid 2610 |
. 2
⊢
(((ω CNF 𝑊)
∘ (𝑦 ∈ {𝑥 ∈ ((ω
↑𝑜 2𝑜) ↑𝑚
𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊))))) ∘ ◡((ω ↑𝑜
2𝑜) CNF 𝑊)) = (((ω CNF 𝑊) ∘ (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜
2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊))))) ∘ ◡((ω ↑𝑜
2𝑜) CNF 𝑊)) |
8 | | eqid 2610 |
. 2
⊢ (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡((𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) ∘ ◡(𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)))))) = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡((𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) ∘ ◡(𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)))))) |
9 | | eqid 2610 |
. 2
⊢ (𝑧 ∈ 2𝑜,
𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)) = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤)) |
10 | | eqid 2610 |
. 2
⊢ (𝑧 ∈ 2𝑜,
𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) = (𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) |
11 | | eqid 2610 |
. 2
⊢
(((ω CNF (2𝑜 ·𝑜 𝑊)) ∘ (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡((𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) ∘ ◡(𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤))))))) ∘ ◡(ω CNF (𝑊 ·𝑜
2𝑜))) = (((ω CNF (2𝑜
·𝑜 𝑊)) ∘ (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡((𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) ∘ ◡(𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤))))))) ∘ ◡(ω CNF (𝑊 ·𝑜
2𝑜))) |
12 | | eqid 2610 |
. 2
⊢ (𝑥 ∈ (ω
↑𝑜 𝑊), 𝑦 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦)) = (𝑥 ∈ (ω ↑𝑜
𝑊), 𝑦 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦)) |
13 | | eqid 2610 |
. 2
⊢ (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) |
14 | | eqid 2610 |
. 2
⊢ (◡(𝑛‘𝑏) ∘ ((((((ω CNF 𝑊) ∘ (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜
2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊))))) ∘ ◡((ω ↑𝑜
2𝑜) CNF 𝑊)) ∘ (((ω CNF
(2𝑜 ·𝑜 𝑊)) ∘ (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡((𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) ∘ ◡(𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤))))))) ∘ ◡(ω CNF (𝑊 ·𝑜
2𝑜)))) ∘ (𝑥 ∈ (ω ↑𝑜
𝑊), 𝑦 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦))) ∘ (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉))) = (◡(𝑛‘𝑏) ∘ ((((((ω CNF 𝑊) ∘ (𝑦 ∈ {𝑥 ∈ ((ω ↑𝑜
2𝑜) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊))))) ∘ ◡((ω ↑𝑜
2𝑜) CNF 𝑊)) ∘ (((ω CNF
(2𝑜 ·𝑜 𝑊)) ∘ (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊
·𝑜 2𝑜)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾
ω) ∘ (𝑦 ∘
◡((𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((2𝑜
·𝑜 𝑤) +𝑜 𝑧)) ∘ ◡(𝑧 ∈ 2𝑜, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·𝑜 𝑧) +𝑜 𝑤))))))) ∘ ◡(ω CNF (𝑊 ·𝑜
2𝑜)))) ∘ (𝑥 ∈ (ω ↑𝑜
𝑊), 𝑦 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑥) +𝑜 𝑦))) ∘ (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉))) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | infxpenc2lem2 8726 |
1
⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |