This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ dom ( ω CNF 𝐴 ) = dom ( ω CNF 𝐴 )
2 eqid ⊢ ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) = ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 )
3 eqid ⊢ OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) = OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) )
4 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
5 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) ) , ∅ )
6 eqid ⊢ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) = ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) )
7 eqid ⊢ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) = ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) )
8 eqid ⊢ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) = ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) )
9 eqid ⊢ ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑣 ) +o 𝑢 ) ) = ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑣 ) +o 𝑢 ) )
10 eqid ⊢ ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑢 ) +o 𝑣 ) ) = ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑢 ) +o 𝑣 ) )
11 eqid ⊢ ( ( ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑣 ) +o 𝑢 ) ) ∘ ◡ ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑢 ) +o 𝑣 ) ) ) ∘ ( seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) = ( ( ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑣 ) +o 𝑢 ) ) ∘ ◡ ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑢 ) +o 𝑣 ) ) ) ∘ ( seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) )
12 eqid ⊢ ( 𝑏 ∈ ( ω ↑o 𝐴 ) ↦ ( ( ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑣 ) +o 𝑢 ) ) ∘ ◡ ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑢 ) +o 𝑣 ) ) ) ∘ ( seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ) = ( 𝑏 ∈ ( ω ↑o 𝐴 ) ↦ ( ( ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑣 ) +o 𝑢 ) ) ∘ ◡ ( 𝑢 ∈ ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) , 𝑣 ∈ ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ ∪ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) ·o 𝑢 ) +o 𝑣 ) ) ) ∘ ( seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ ( ( 𝑥 ∈ ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( ( ( ω ↑o ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) ‘ ( OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑥 ) ) ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 ) supp ∅ ) ) ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 cnfcom3clem ⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )