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

Metamath Proof Explorer

Theorem cantnff1o

Description: Simplify the isomorphism of cantnf to simple bijection. (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Hypotheses cantnff1o.1 
|- S = dom ( A CNF B )
cantnff1o.2 
|- ( ph -> A e. On )
cantnff1o.3 
|- ( ph -> B e. On )
Assertion cantnff1o 
|- ( ph -> ( A CNF B ) : S -1-1-onto-> ( A ^o B ) )

Proof

Step Hyp Ref Expression
1 cantnff1o.1 
 |-  S = dom ( A CNF B )
2 cantnff1o.2 
 |-  ( ph -> A e. On )
3 cantnff1o.3 
 |-  ( ph -> B e. On )
4 eqid 
 |-  { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 1 2 3 4 cantnf 
 |-  ( ph -> ( A CNF B ) Isom { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } , _E ( S , ( A ^o B ) ) )
6 isof1o 
 |-  ( ( A CNF B ) Isom { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } , _E ( S , ( A ^o B ) ) -> ( A CNF B ) : S -1-1-onto-> ( A ^o B ) )
7 5 6 syl 
 |-  ( ph -> ( A CNF B ) : S -1-1-onto-> ( A ^o B ) )