ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  hashfacen Unicode version

Theorem hashfacen 10800
Description: The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)
Assertion
Ref Expression
hashfacen  |-  ( ( A  ~~  B  /\  C  ~~  D )  ->  { f  |  f : A -1-1-onto-> C }  ~~  {
f  |  f : B -1-1-onto-> D } )
Distinct variable groups:    A, f    B, f    C, f    D, f

Proof of Theorem hashfacen
Dummy variables  g  h  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 6741 . 2  |-  ( A 
~~  B  <->  E. g 
g : A -1-1-onto-> B )
2 bren 6741 . 2  |-  ( C 
~~  D  <->  E. h  h : C -1-1-onto-> D )
3 eeanv 1932 . . 3  |-  ( E. g E. h ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  <->  ( E. g  g : A -1-1-onto-> B  /\  E. h  h : C -1-1-onto-> D ) )
4 f1odm 5461 . . . . . . . 8  |-  ( h : C -1-1-onto-> D  ->  dom  h  =  C )
5 vex 2740 . . . . . . . . 9  |-  h  e. 
_V
65dmex 4889 . . . . . . . 8  |-  dom  h  e.  _V
74, 6eqeltrrdi 2269 . . . . . . 7  |-  ( h : C -1-1-onto-> D  ->  C  e.  _V )
8 f1odm 5461 . . . . . . . 8  |-  ( g : A -1-1-onto-> B  ->  dom  g  =  A )
9 vex 2740 . . . . . . . . 9  |-  g  e. 
_V
109dmex 4889 . . . . . . . 8  |-  dom  g  e.  _V
118, 10eqeltrrdi 2269 . . . . . . 7  |-  ( g : A -1-1-onto-> B  ->  A  e.  _V )
12 fnmap 6649 . . . . . . . 8  |-  ^m  Fn  ( _V  X.  _V )
13 fnovex 5902 . . . . . . . 8  |-  ( (  ^m  Fn  ( _V 
X.  _V )  /\  C  e.  _V  /\  A  e. 
_V )  ->  ( C  ^m  A )  e. 
_V )
1412, 13mp3an1 1324 . . . . . . 7  |-  ( ( C  e.  _V  /\  A  e.  _V )  ->  ( C  ^m  A
)  e.  _V )
157, 11, 14syl2anr 290 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  ( C  ^m  A )  e. 
_V )
16 f1of 5457 . . . . . . . 8  |-  ( f : A -1-1-onto-> C  ->  f : A
--> C )
17 elmapg 6655 . . . . . . . . 9  |-  ( ( C  e.  _V  /\  A  e.  _V )  ->  ( f  e.  ( C  ^m  A )  <-> 
f : A --> C ) )
187, 11, 17syl2anr 290 . . . . . . . 8  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
f  e.  ( C  ^m  A )  <->  f : A
--> C ) )
1916, 18syl5ibr 156 . . . . . . 7  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
f : A -1-1-onto-> C  -> 
f  e.  ( C  ^m  A ) ) )
2019abssdv 3229 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  { f  |  f : A -1-1-onto-> C }  C_  ( C  ^m  A ) )
2115, 20ssexd 4140 . . . . 5  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  { f  |  f : A -1-1-onto-> C }  e.  _V )
22 f1ofo 5464 . . . . . . . . 9  |-  ( h : C -1-1-onto-> D  ->  h : C -onto-> D )
23 forn 5437 . . . . . . . . 9  |-  ( h : C -onto-> D  ->  ran  h  =  D )
2422, 23syl 14 . . . . . . . 8  |-  ( h : C -1-1-onto-> D  ->  ran  h  =  D )
255rnex 4890 . . . . . . . 8  |-  ran  h  e.  _V
2624, 25eqeltrrdi 2269 . . . . . . 7  |-  ( h : C -1-1-onto-> D  ->  D  e.  _V )
27 f1ofo 5464 . . . . . . . . 9  |-  ( g : A -1-1-onto-> B  ->  g : A -onto-> B )
28 forn 5437 . . . . . . . . 9  |-  ( g : A -onto-> B  ->  ran  g  =  B
)
2927, 28syl 14 . . . . . . . 8  |-  ( g : A -1-1-onto-> B  ->  ran  g  =  B )
309rnex 4890 . . . . . . . 8  |-  ran  g  e.  _V
3129, 30eqeltrrdi 2269 . . . . . . 7  |-  ( g : A -1-1-onto-> B  ->  B  e.  _V )
32 fnovex 5902 . . . . . . . 8  |-  ( (  ^m  Fn  ( _V 
X.  _V )  /\  D  e.  _V  /\  B  e. 
_V )  ->  ( D  ^m  B )  e. 
_V )
3312, 32mp3an1 1324 . . . . . . 7  |-  ( ( D  e.  _V  /\  B  e.  _V )  ->  ( D  ^m  B
)  e.  _V )
3426, 31, 33syl2anr 290 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  ( D  ^m  B )  e. 
_V )
35 f1of 5457 . . . . . . . 8  |-  ( f : B -1-1-onto-> D  ->  f : B
--> D )
36 elmapg 6655 . . . . . . . . 9  |-  ( ( D  e.  _V  /\  B  e.  _V )  ->  ( f  e.  ( D  ^m  B )  <-> 
f : B --> D ) )
3726, 31, 36syl2anr 290 . . . . . . . 8  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
f  e.  ( D  ^m  B )  <->  f : B
--> D ) )
3835, 37syl5ibr 156 . . . . . . 7  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
f : B -1-1-onto-> D  -> 
f  e.  ( D  ^m  B ) ) )
3938abssdv 3229 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  { f  |  f : B -1-1-onto-> D }  C_  ( D  ^m  B ) )
4034, 39ssexd 4140 . . . . 5  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  { f  |  f : B -1-1-onto-> D }  e.  _V )
41 f1oco 5480 . . . . . . . . 9  |-  ( ( h : C -1-1-onto-> D  /\  x : A -1-1-onto-> C )  ->  (
h  o.  x ) : A -1-1-onto-> D )
4241adantll 476 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  x : A -1-1-onto-> C
)  ->  ( h  o.  x ) : A -1-1-onto-> D
)
43 f1ocnv 5470 . . . . . . . . 9  |-  ( g : A -1-1-onto-> B  ->  `' g : B -1-1-onto-> A )
4443ad2antrr 488 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  x : A -1-1-onto-> C
)  ->  `' g : B -1-1-onto-> A )
45 f1oco 5480 . . . . . . . 8  |-  ( ( ( h  o.  x
) : A -1-1-onto-> D  /\  `' g : B -1-1-onto-> A
)  ->  ( (
h  o.  x )  o.  `' g ) : B -1-1-onto-> D )
4642, 44, 45syl2anc 411 . . . . . . 7  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  x : A -1-1-onto-> C
)  ->  ( (
h  o.  x )  o.  `' g ) : B -1-1-onto-> D )
4746ex 115 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
x : A -1-1-onto-> C  -> 
( ( h  o.  x )  o.  `' g ) : B -1-1-onto-> D
) )
48 vex 2740 . . . . . . 7  |-  x  e. 
_V
49 f1oeq1 5445 . . . . . . 7  |-  ( f  =  x  ->  (
f : A -1-1-onto-> C  <->  x : A
-1-1-onto-> C ) )
5048, 49elab 2881 . . . . . 6  |-  ( x  e.  { f  |  f : A -1-1-onto-> C }  <->  x : A -1-1-onto-> C )
515, 48coex 5170 . . . . . . . 8  |-  ( h  o.  x )  e. 
_V
529cnvex 5163 . . . . . . . 8  |-  `' g  e.  _V
5351, 52coex 5170 . . . . . . 7  |-  ( ( h  o.  x )  o.  `' g )  e.  _V
54 f1oeq1 5445 . . . . . . 7  |-  ( f  =  ( ( h  o.  x )  o.  `' g )  -> 
( f : B -1-1-onto-> D  <->  ( ( h  o.  x
)  o.  `' g ) : B -1-1-onto-> D ) )
5553, 54elab 2881 . . . . . 6  |-  ( ( ( h  o.  x
)  o.  `' g )  e.  { f  |  f : B -1-1-onto-> D } 
<->  ( ( h  o.  x )  o.  `' g ) : B -1-1-onto-> D
)
5647, 50, 553imtr4g 205 . . . . 5  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
x  e.  { f  |  f : A -1-1-onto-> C }  ->  ( ( h  o.  x )  o.  `' g )  e. 
{ f  |  f : B -1-1-onto-> D } ) )
57 f1ocnv 5470 . . . . . . . . 9  |-  ( h : C -1-1-onto-> D  ->  `' h : D -1-1-onto-> C )
5857ad2antlr 489 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  y : B -1-1-onto-> D
)  ->  `' h : D -1-1-onto-> C )
59 f1oco 5480 . . . . . . . . . 10  |-  ( ( y : B -1-1-onto-> D  /\  g : A -1-1-onto-> B )  ->  (
y  o.  g ) : A -1-1-onto-> D )
6059ancoms 268 . . . . . . . . 9  |-  ( ( g : A -1-1-onto-> B  /\  y : B -1-1-onto-> D )  ->  (
y  o.  g ) : A -1-1-onto-> D )
6160adantlr 477 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  y : B -1-1-onto-> D
)  ->  ( y  o.  g ) : A -1-1-onto-> D
)
62 f1oco 5480 . . . . . . . 8  |-  ( ( `' h : D -1-1-onto-> C  /\  ( y  o.  g
) : A -1-1-onto-> D )  ->  ( `' h  o.  ( y  o.  g
) ) : A -1-1-onto-> C
)
6358, 61, 62syl2anc 411 . . . . . . 7  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  y : B -1-1-onto-> D
)  ->  ( `' h  o.  ( y  o.  g ) ) : A -1-1-onto-> C )
6463ex 115 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
y : B -1-1-onto-> D  -> 
( `' h  o.  ( y  o.  g
) ) : A -1-1-onto-> C
) )
65 vex 2740 . . . . . . 7  |-  y  e. 
_V
66 f1oeq1 5445 . . . . . . 7  |-  ( f  =  y  ->  (
f : B -1-1-onto-> D  <->  y : B
-1-1-onto-> D ) )
6765, 66elab 2881 . . . . . 6  |-  ( y  e.  { f  |  f : B -1-1-onto-> D }  <->  y : B -1-1-onto-> D )
685cnvex 5163 . . . . . . . 8  |-  `' h  e.  _V
6965, 9coex 5170 . . . . . . . 8  |-  ( y  o.  g )  e. 
_V
7068, 69coex 5170 . . . . . . 7  |-  ( `' h  o.  ( y  o.  g ) )  e.  _V
71 f1oeq1 5445 . . . . . . 7  |-  ( f  =  ( `' h  o.  ( y  o.  g
) )  ->  (
f : A -1-1-onto-> C  <->  ( `' h  o.  ( y  o.  g ) ) : A -1-1-onto-> C ) )
7270, 71elab 2881 . . . . . 6  |-  ( ( `' h  o.  (
y  o.  g ) )  e.  { f  |  f : A -1-1-onto-> C } 
<->  ( `' h  o.  ( y  o.  g
) ) : A -1-1-onto-> C
)
7364, 67, 723imtr4g 205 . . . . 5  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
y  e.  { f  |  f : B -1-1-onto-> D }  ->  ( `' h  o.  ( y  o.  g
) )  e.  {
f  |  f : A -1-1-onto-> C } ) )
7450, 67anbi12i 460 . . . . . 6  |-  ( ( x  e.  { f  |  f : A -1-1-onto-> C }  /\  y  e.  {
f  |  f : B -1-1-onto-> D } )  <->  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )
75 coass 5143 . . . . . . . . . . 11  |-  ( ( ( h  o.  x
)  o.  `' g )  o.  g )  =  ( ( h  o.  x )  o.  ( `' g  o.  g ) )
76 f1ococnv1 5486 . . . . . . . . . . . . . 14  |-  ( g : A -1-1-onto-> B  ->  ( `' g  o.  g )  =  (  _I  |`  A ) )
7776ad2antrr 488 . . . . . . . . . . . . 13  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( `' g  o.  g )  =  (  _I  |`  A )
)
7877coeq2d 4785 . . . . . . . . . . . 12  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  o.  ( `' g  o.  g
) )  =  ( ( h  o.  x
)  o.  (  _I  |`  A ) ) )
7942adantrr 479 . . . . . . . . . . . . 13  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( h  o.  x
) : A -1-1-onto-> D )
80 f1of 5457 . . . . . . . . . . . . 13  |-  ( ( h  o.  x ) : A -1-1-onto-> D  ->  ( h  o.  x ) : A --> D )
81 fcoi1 5392 . . . . . . . . . . . . 13  |-  ( ( h  o.  x ) : A --> D  -> 
( ( h  o.  x )  o.  (  _I  |`  A ) )  =  ( h  o.  x ) )
8279, 80, 813syl 17 . . . . . . . . . . . 12  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  o.  (  _I  |`  A ) )  =  ( h  o.  x ) )
8378, 82eqtrd 2210 . . . . . . . . . . 11  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  o.  ( `' g  o.  g
) )  =  ( h  o.  x ) )
8475, 83eqtr2id 2223 . . . . . . . . . 10  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( h  o.  x
)  =  ( ( ( h  o.  x
)  o.  `' g )  o.  g ) )
85 coass 5143 . . . . . . . . . . 11  |-  ( ( h  o.  `' h
)  o.  ( y  o.  g ) )  =  ( h  o.  ( `' h  o.  ( y  o.  g
) ) )
86 f1ococnv2 5484 . . . . . . . . . . . . . 14  |-  ( h : C -1-1-onto-> D  ->  ( h  o.  `' h )  =  (  _I  |`  D )
)
8786ad2antlr 489 . . . . . . . . . . . . 13  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( h  o.  `' h )  =  (  _I  |`  D )
)
8887coeq1d 4784 . . . . . . . . . . . 12  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  `' h )  o.  (
y  o.  g ) )  =  ( (  _I  |`  D )  o.  ( y  o.  g
) ) )
8961adantrl 478 . . . . . . . . . . . . 13  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( y  o.  g
) : A -1-1-onto-> D )
90 f1of 5457 . . . . . . . . . . . . 13  |-  ( ( y  o.  g ) : A -1-1-onto-> D  ->  ( y  o.  g ) : A --> D )
91 fcoi2 5393 . . . . . . . . . . . . 13  |-  ( ( y  o.  g ) : A --> D  -> 
( (  _I  |`  D )  o.  ( y  o.  g ) )  =  ( y  o.  g
) )
9289, 90, 913syl 17 . . . . . . . . . . . 12  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( (  _I  |`  D )  o.  ( y  o.  g ) )  =  ( y  o.  g
) )
9388, 92eqtrd 2210 . . . . . . . . . . 11  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  `' h )  o.  (
y  o.  g ) )  =  ( y  o.  g ) )
9485, 93eqtr3id 2224 . . . . . . . . . 10  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( h  o.  ( `' h  o.  (
y  o.  g ) ) )  =  ( y  o.  g ) )
9584, 94eqeq12d 2192 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  =  ( h  o.  ( `' h  o.  ( y  o.  g ) ) )  <->  ( ( ( h  o.  x )  o.  `' g )  o.  g )  =  ( y  o.  g
) ) )
96 eqcom 2179 . . . . . . . . 9  |-  ( ( ( ( h  o.  x )  o.  `' g )  o.  g
)  =  ( y  o.  g )  <->  ( y  o.  g )  =  ( ( ( h  o.  x )  o.  `' g )  o.  g
) )
9795, 96bitrdi 196 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  =  ( h  o.  ( `' h  o.  ( y  o.  g ) ) )  <->  ( y  o.  g )  =  ( ( ( h  o.  x )  o.  `' g )  o.  g
) ) )
98 f1of1 5456 . . . . . . . . . 10  |-  ( h : C -1-1-onto-> D  ->  h : C -1-1-> D )
9998ad2antlr 489 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  ->  h : C -1-1-> D )
100 f1of 5457 . . . . . . . . . 10  |-  ( x : A -1-1-onto-> C  ->  x : A
--> C )
101100ad2antrl 490 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  ->  x : A --> C )
10263adantrl 478 . . . . . . . . . 10  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( `' h  o.  ( y  o.  g
) ) : A -1-1-onto-> C
)
103 f1of 5457 . . . . . . . . . 10  |-  ( ( `' h  o.  (
y  o.  g ) ) : A -1-1-onto-> C  -> 
( `' h  o.  ( y  o.  g
) ) : A --> C )
104102, 103syl 14 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( `' h  o.  ( y  o.  g
) ) : A --> C )
105 cocan1 5782 . . . . . . . . 9  |-  ( ( h : C -1-1-> D  /\  x : A --> C  /\  ( `' h  o.  (
y  o.  g ) ) : A --> C )  ->  ( ( h  o.  x )  =  ( h  o.  ( `' h  o.  (
y  o.  g ) ) )  <->  x  =  ( `' h  o.  (
y  o.  g ) ) ) )
10699, 101, 104, 105syl3anc 1238 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  =  ( h  o.  ( `' h  o.  ( y  o.  g ) ) )  <->  x  =  ( `' h  o.  (
y  o.  g ) ) ) )
10727ad2antrr 488 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
g : A -onto-> B
)
108 f1ofn 5458 . . . . . . . . . 10  |-  ( y : B -1-1-onto-> D  ->  y  Fn  B )
109108ad2antll 491 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
y  Fn  B )
11046adantrr 479 . . . . . . . . . 10  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  o.  `' g ) : B -1-1-onto-> D
)
111 f1ofn 5458 . . . . . . . . . 10  |-  ( ( ( h  o.  x
)  o.  `' g ) : B -1-1-onto-> D  -> 
( ( h  o.  x )  o.  `' g )  Fn  B
)
112110, 111syl 14 . . . . . . . . 9  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( h  o.  x )  o.  `' g )  Fn  B
)
113 cocan2 5783 . . . . . . . . 9  |-  ( ( g : A -onto-> B  /\  y  Fn  B  /\  ( ( h  o.  x )  o.  `' g )  Fn  B
)  ->  ( (
y  o.  g )  =  ( ( ( h  o.  x )  o.  `' g )  o.  g )  <->  y  =  ( ( h  o.  x )  o.  `' g ) ) )
114107, 109, 112, 113syl3anc 1238 . . . . . . . 8  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( ( y  o.  g )  =  ( ( ( h  o.  x )  o.  `' g )  o.  g
)  <->  y  =  ( ( h  o.  x
)  o.  `' g ) ) )
11597, 106, 1143bitr3d 218 . . . . . . 7  |-  ( ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  /\  ( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D ) )  -> 
( x  =  ( `' h  o.  (
y  o.  g ) )  <->  y  =  ( ( h  o.  x
)  o.  `' g ) ) )
116115ex 115 . . . . . 6  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
( x : A -1-1-onto-> C  /\  y : B -1-1-onto-> D )  ->  ( x  =  ( `' h  o.  ( y  o.  g
) )  <->  y  =  ( ( h  o.  x )  o.  `' g ) ) ) )
11774, 116biimtrid 152 . . . . 5  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  (
( x  e.  {
f  |  f : A -1-1-onto-> C }  /\  y  e.  { f  |  f : B -1-1-onto-> D } )  -> 
( x  =  ( `' h  o.  (
y  o.  g ) )  <->  y  =  ( ( h  o.  x
)  o.  `' g ) ) ) )
11821, 40, 56, 73, 117en3d 6763 . . . 4  |-  ( ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  { f  |  f : A -1-1-onto-> C }  ~~  { f  |  f : B -1-1-onto-> D }
)
119118exlimivv 1896 . . 3  |-  ( E. g E. h ( g : A -1-1-onto-> B  /\  h : C -1-1-onto-> D )  ->  { f  |  f : A -1-1-onto-> C }  ~~  { f  |  f : B -1-1-onto-> D }
)
1203, 119sylbir 135 . 2  |-  ( ( E. g  g : A -1-1-onto-> B  /\  E. h  h : C -1-1-onto-> D )  ->  { f  |  f : A -1-1-onto-> C }  ~~  { f  |  f : B -1-1-onto-> D }
)
1211, 2, 120syl2anb 291 1  |-  ( ( A  ~~  B  /\  C  ~~  D )  ->  { f  |  f : A -1-1-onto-> C }  ~~  {
f  |  f : B -1-1-onto-> D } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1353   E.wex 1492    e. wcel 2148   {cab 2163   _Vcvv 2737   class class class wbr 4000    _I cid 4285    X. cxp 4621   `'ccnv 4622   dom cdm 4623   ran crn 4624    |` cres 4625    o. ccom 4627    Fn wfn 5207   -->wf 5208   -1-1->wf1 5209   -onto->wfo 5210   -1-1-onto->wf1o 5211  (class class class)co 5869    ^m cmap 6642    ~~ cen 6732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-map 6644  df-en 6735
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator