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 e. On -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  dom ( _om CNF A ) = dom ( _om CNF A )
2 eqid 
 |-  ( `' ( _om CNF A ) ` b ) = ( `' ( _om CNF A ) ` b )
3 eqid 
 |-  OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) = OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) )
4 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
5 eqid 
 |-  seqom ( ( k e. _V , f e. _V |-> ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) ) , (/) ) = seqom ( ( k e. _V , f e. _V |-> ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) ) , (/) )
6 eqid 
 |-  ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) = ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) )
7 eqid 
 |-  ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) = ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) )
8 eqid 
 |-  ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) = ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) )
9 eqid 
 |-  ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o v ) +o u ) ) = ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o v ) +o u ) )
10 eqid 
 |-  ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o u ) +o v ) ) = ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o u ) +o v ) )
11 eqid 
 |-  ( ( ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o v ) +o u ) ) o. `' ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o u ) +o v ) ) ) o. ( seqom ( ( k e. _V , f e. _V |-> ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) ) , (/) ) ` dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) = ( ( ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o v ) +o u ) ) o. `' ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o u ) +o v ) ) ) o. ( seqom ( ( k e. _V , f e. _V |-> ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) ) , (/) ) ` dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) )
12 eqid 
 |-  ( b e. ( _om ^o A ) |-> ( ( ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o v ) +o u ) ) o. `' ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o u ) +o v ) ) ) o. ( seqom ( ( k e. _V , f e. _V |-> ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) ) , (/) ) ` dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) ) = ( b e. ( _om ^o A ) |-> ( ( ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o v ) +o u ) ) o. `' ( u e. ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) , v e. ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` U. dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) .o u ) +o v ) ) ) o. ( seqom ( ( k e. _V , f e. _V |-> ( ( x e. ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( ( ( _om ^o ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) .o ( ( `' ( _om CNF A ) ` b ) ` ( OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ` k ) ) ) +o x ) ) ) ) , (/) ) ` dom OrdIso ( _E , ( ( `' ( _om CNF A ) ` b ) supp (/) ) ) ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 cnfcom3clem 
 |-  ( A e. On -> E. g A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( g ` b ) : b -1-1-onto-> ( _om ^o w ) ) )