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 ๐‘ค ) ) )