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 ⁡ ω CNF A = dom ⁡ ω CNF A
2 eqid ⊢ ω CNF A -1 ⁡ b = ω CNF A -1 ⁡ b
3 eqid ⊢ OrdIso E ω CNF A -1 ⁡ b supp ∅ = OrdIso E ω CNF A -1 ⁡ b supp ∅
4 eqid ⊢ seq ω k ∈ V , z ∈ V ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 z ∅
5 eqid ⊢ seq ω k ∈ V , f ∈ V ⟼ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 ∅ = seq ω k ∈ V , f ∈ V ⟼ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 ∅
6 eqid ⊢ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k = ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k
7 eqid ⊢ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 = x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1
8 eqid ⊢ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ = OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅
9 eqid ⊢ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 v + 𝑜 u = u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 v + 𝑜 u
10 eqid ⊢ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 u + 𝑜 v = u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 u + 𝑜 v
11 eqid ⊢ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 v + 𝑜 u ∘ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 u + 𝑜 v -1 ∘ seq ω k ∈ V , f ∈ V ⟼ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 ∅ ⁡ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ = u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 v + 𝑜 u ∘ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 u + 𝑜 v -1 ∘ seq ω k ∈ V , f ∈ V ⟼ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 ∅ ⁡ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅
12 eqid ⊢ b ∈ ω ↑ 𝑜 A ⟼ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 v + 𝑜 u ∘ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 u + 𝑜 v -1 ∘ seq ω k ∈ V , f ∈ V ⟼ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 ∅ ⁡ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ = b ∈ ω ↑ 𝑜 A ⟼ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 v + 𝑜 u ∘ u ∈ ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ , v ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ ⋃ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⋅ 𝑜 u + 𝑜 v -1 ∘ seq ω k ∈ V , f ∈ V ⟼ x ∈ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ ω ↑ 𝑜 OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k ⋅ 𝑜 ω CNF A -1 ⁡ b ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅ ⁡ k + 𝑜 x -1 ∅ ⁡ dom ⁡ OrdIso E ω CNF A -1 ⁡ b supp ∅
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