Metamath Proof Explorer

Theorem cnfcom3c

Description: Wrap the construction of cnfcom3 into an existential quantifier. For any _om C_ b , there is a bijection from b to some power of _om . Furthermore, this bijection iscanonical , which means that we can find a single function g which will give such bijections for every b less than some arbitrarily large bound A . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Assertion cnfcom3c ⊢A∈On→∃g∀b∈Aω⊆b→∃w∈On∖1𝑜g⁡b:b⟶1-1 ontoω↑𝑜w

Proof

Step Hyp Ref Expression
1 eqid ⊢dom⁡ωCNFA=dom⁡ωCNFA
2 eqid ⊢ωCNFA-1⁡b=ωCNFA-1⁡b
3 eqid ⊢OrdIsoEωCNFA-1⁡bsupp∅=OrdIsoEωCNFA-1⁡bsupp∅
4 eqid ⊢seqωk∈V,z∈V⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜z∅=seqωk∈V,z∈V⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜z∅
5 eqid ⊢seqωk∈V,f∈V⟼x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1∅=seqωk∈V,f∈V⟼x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1∅
6 eqid ⊢ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k=ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k
7 eqid ⊢x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1=x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1
8 eqid ⊢OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅=OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅
9 eqid ⊢u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜v+𝑜u=u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜v+𝑜u
10 eqid ⊢u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜u+𝑜v=u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜u+𝑜v
11 eqid ⊢u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜v+𝑜u∘u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜u+𝑜v-1∘seqωk∈V,f∈V⟼x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1∅⁡dom⁡OrdIsoEωCNFA-1⁡bsupp∅=u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜v+𝑜u∘u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜u+𝑜v-1∘seqωk∈V,f∈V⟼x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1∅⁡dom⁡OrdIsoEωCNFA-1⁡bsupp∅
12 eqid ⊢b∈ω↑𝑜A⟼u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜v+𝑜u∘u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜u+𝑜v-1∘seqωk∈V,f∈V⟼x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1∅⁡dom⁡OrdIsoEωCNFA-1⁡bsupp∅=b∈ω↑𝑜A⟼u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜v+𝑜u∘u∈ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅,v∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡⋃dom⁡OrdIsoEωCNFA-1⁡bsupp∅⋅𝑜u+𝑜v-1∘seqωk∈V,f∈V⟼x∈ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k⟼dom⁡f+𝑜x∪x∈dom⁡f⟼ω↑𝑜OrdIsoEωCNFA-1⁡bsupp∅⁡k⋅𝑜ωCNFA-1⁡b⁡OrdIsoEωCNFA-1⁡bsupp∅⁡k+𝑜x-1∅⁡dom⁡OrdIsoEωCNFA-1⁡bsupp∅
13 1 2 3 4 5 6 7 8 9 10 11 12 cnfcom3clem ⊢A∈On→∃g∀b∈Aω⊆b→∃w∈On∖1𝑜g⁡b:b⟶1-1 ontoω↑𝑜w