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