Metamath Proof Explorer

Theorem infxpenc2lem3

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc2.1 ⊢φ→A∈On
infxpenc2.2 ⊢φ→∀b∈Aω⊆b→∃w∈On∖1𝑜n⁡b:b⟶1-1 ontoω↑𝑜w
infxpenc2.3 ⊢W=x∈On∖1𝑜⟼ω↑𝑜x-1⁡ran⁡n⁡b
infxpenc2.4 ⊢φ→F:ω↑𝑜2𝑜⟶1-1 ontoω
infxpenc2.5 ⊢φ→F⁡∅=∅
Assertion infxpenc2lem3 ⊢φ→∃g∀b∈Aω⊆b→g⁡b:b×b⟶1-1 ontob

Proof

Step Hyp Ref Expression
1 infxpenc2.1 ⊢φ→A∈On
2 infxpenc2.2 ⊢φ→∀b∈Aω⊆b→∃w∈On∖1𝑜n⁡b:b⟶1-1 ontoω↑𝑜w
3 infxpenc2.3 ⊢W=x∈On∖1𝑜⟼ω↑𝑜x-1⁡ran⁡n⁡b
4 infxpenc2.4 ⊢φ→F:ω↑𝑜2𝑜⟶1-1 ontoω
5 infxpenc2.5 ⊢φ→F⁡∅=∅
6 eqid ⊢y∈x∈ω↑𝑜2𝑜W|finSupp∅⁡x⟼F∘y∘I↾W-1=y∈x∈ω↑𝑜2𝑜W|finSupp∅⁡x⟼F∘y∘I↾W-1
7 eqid ⊢ωCNFW∘y∈x∈ω↑𝑜2𝑜W|finSupp∅⁡x⟼F∘y∘I↾W-1∘ω↑𝑜2𝑜CNFW-1=ωCNFW∘y∈x∈ω↑𝑜2𝑜W|finSupp∅⁡x⟼F∘y∘I↾W-1∘ω↑𝑜2𝑜CNFW-1
8 eqid ⊢y∈x∈ωW⋅𝑜2𝑜|finSupp∅⁡x⟼I↾ω∘y∘z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z∘z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w-1-1=y∈x∈ωW⋅𝑜2𝑜|finSupp∅⁡x⟼I↾ω∘y∘z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z∘z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w-1-1
9 eqid ⊢z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w=z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w
10 eqid ⊢z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z=z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z
11 eqid ⊢ωCNF2𝑜⋅𝑜W∘y∈x∈ωW⋅𝑜2𝑜|finSupp∅⁡x⟼I↾ω∘y∘z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z∘z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w-1-1∘ωCNFW⋅𝑜2𝑜-1=ωCNF2𝑜⋅𝑜W∘y∈x∈ωW⋅𝑜2𝑜|finSupp∅⁡x⟼I↾ω∘y∘z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z∘z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w-1-1∘ωCNFW⋅𝑜2𝑜-1
12 eqid ⊢x∈ω↑𝑜W,y∈ω↑𝑜W⟼ω↑𝑜W⋅𝑜x+𝑜y=x∈ω↑𝑜W,y∈ω↑𝑜W⟼ω↑𝑜W⋅𝑜x+𝑜y
13 eqid ⊢x∈b,y∈b⟼n⁡b⁡xn⁡b⁡y=x∈b,y∈b⟼n⁡b⁡xn⁡b⁡y
14 eqid ⊢n⁡b-1∘ωCNFW∘y∈x∈ω↑𝑜2𝑜W|finSupp∅⁡x⟼F∘y∘I↾W-1∘ω↑𝑜2𝑜CNFW-1∘ωCNF2𝑜⋅𝑜W∘y∈x∈ωW⋅𝑜2𝑜|finSupp∅⁡x⟼I↾ω∘y∘z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z∘z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w-1-1∘ωCNFW⋅𝑜2𝑜-1∘x∈ω↑𝑜W,y∈ω↑𝑜W⟼ω↑𝑜W⋅𝑜x+𝑜y∘x∈b,y∈b⟼n⁡b⁡xn⁡b⁡y=n⁡b-1∘ωCNFW∘y∈x∈ω↑𝑜2𝑜W|finSupp∅⁡x⟼F∘y∘I↾W-1∘ω↑𝑜2𝑜CNFW-1∘ωCNF2𝑜⋅𝑜W∘y∈x∈ωW⋅𝑜2𝑜|finSupp∅⁡x⟼I↾ω∘y∘z∈2𝑜,w∈W⟼2𝑜⋅𝑜w+𝑜z∘z∈2𝑜,w∈W⟼W⋅𝑜z+𝑜w-1-1∘ωCNFW⋅𝑜2𝑜-1∘x∈ω↑𝑜W,y∈ω↑𝑜W⟼ω↑𝑜W⋅𝑜x+𝑜y∘x∈b,y∈b⟼n⁡b⁡xn⁡b⁡y
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 infxpenc2lem2 ⊢φ→∃g∀b∈Aω⊆b→g⁡b:b×b⟶1-1 ontob