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 𝑤 ) ) )