MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashdom Structured version   Unicode version

Theorem hashdom 12134
Description: Dominance relation for the size function. (Contributed by Mario Carneiro, 22-Sep-2013.) (Revised by Mario Carneiro, 22-Apr-2015.)
Assertion
Ref Expression
hashdom  |-  ( ( A  e.  Fin  /\  B  e.  V )  ->  ( ( # `  A
)  <_  ( # `  B
)  <->  A  ~<_  B )
)

Proof of Theorem hashdom
Dummy variables  x  f  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfi 11786 . . . . . . . 8  |-  ( 1 ... ( ( # `  B )  -  ( # `
 A ) ) )  e.  Fin
2 ficardom 8123 . . . . . . . 8  |-  ( ( 1 ... ( (
# `  B )  -  ( # `  A
) ) )  e. 
Fin  ->  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) )  e.  om )
31, 2ax-mp 5 . . . . . . 7  |-  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) )  e.  om
4 eqid 2438 . . . . . . . . . . . . . 14  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om )
54hashgval 12098 . . . . . . . . . . . . 13  |-  ( A  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  =  ( # `  A
) )
65ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  =  ( # `  A
) )
74hashgval 12098 . . . . . . . . . . . . . 14  |-  ( ( 1 ... ( (
# `  B )  -  ( # `  A
) ) )  e. 
Fin  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) )  =  ( # `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) )
81, 7ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) )  =  ( # `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) )
9 hashcl 12118 . . . . . . . . . . . . . . . 16  |-  ( A  e.  Fin  ->  ( # `
 A )  e. 
NN0 )
109ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( # `
 A )  e. 
NN0 )
11 hashcl 12118 . . . . . . . . . . . . . . . 16  |-  ( B  e.  Fin  ->  ( # `
 B )  e. 
NN0 )
1211ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( # `
 B )  e. 
NN0 )
13 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( # `
 A )  <_ 
( # `  B ) )
14 nn0sub2 10697 . . . . . . . . . . . . . . 15  |-  ( ( ( # `  A
)  e.  NN0  /\  ( # `  B )  e.  NN0  /\  ( # `
 A )  <_ 
( # `  B ) )  ->  ( ( # `
 B )  -  ( # `  A ) )  e.  NN0 )
1510, 12, 13, 14syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( # `  B )  -  ( # `  A
) )  e.  NN0 )
16 hashfz1 12109 . . . . . . . . . . . . . 14  |-  ( ( ( # `  B
)  -  ( # `  A ) )  e. 
NN0  ->  ( # `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) )  =  ( ( # `  B
)  -  ( # `  A ) ) )
1715, 16syl 16 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( # `
 ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) )  =  ( (
# `  B )  -  ( # `  A
) ) )
188, 17syl5eq 2482 . . . . . . . . . . . 12  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) ) )  =  ( ( # `  B
)  -  ( # `  A ) ) )
196, 18oveq12d 6104 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  A
) )  +  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) ) ) )  =  ( ( # `  A
)  +  ( (
# `  B )  -  ( # `  A
) ) ) )
209nn0cnd 10630 . . . . . . . . . . . . 13  |-  ( A  e.  Fin  ->  ( # `
 A )  e.  CC )
2111nn0cnd 10630 . . . . . . . . . . . . 13  |-  ( B  e.  Fin  ->  ( # `
 B )  e.  CC )
22 pncan3 9610 . . . . . . . . . . . . 13  |-  ( ( ( # `  A
)  e.  CC  /\  ( # `  B )  e.  CC )  -> 
( ( # `  A
)  +  ( (
# `  B )  -  ( # `  A
) ) )  =  ( # `  B
) )
2320, 21, 22syl2an 477 . . . . . . . . . . . 12  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  +  ( (
# `  B )  -  ( # `  A
) ) )  =  ( # `  B
) )
2423adantr 465 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( # `  A )  +  ( ( # `  B )  -  ( # `
 A ) ) )  =  ( # `  B ) )
2519, 24eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  A
) )  +  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) ) ) )  =  ( # `  B
) )
26 ficardom 8123 . . . . . . . . . . . 12  |-  ( A  e.  Fin  ->  ( card `  A )  e. 
om )
2726ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( card `  A )  e. 
om )
284hashgadd 12132 . . . . . . . . . . 11  |-  ( ( ( card `  A
)  e.  om  /\  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) )  e.  om )  ->  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) )  =  ( ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  A
) )  +  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) ) ) ) )
2927, 3, 28sylancl 662 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  (
( card `  A )  +o  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) ) )  =  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  +  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) ) ) )
304hashgval 12098 . . . . . . . . . . 11  |-  ( B  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  B ) )  =  ( # `  B
) )
3130ad2antlr 726 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  B ) )  =  ( # `  B
) )
3225, 29, 313eqtr4d 2480 . . . . . . . . 9  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  (
( card `  A )  +o  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) ) )  =  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  B
) ) )
3332fveq2d 5690 . . . . . . . 8  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) ) )  =  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  B
) ) ) )
344hashgf1o 11785 . . . . . . . . 9  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0
35 nnacl 7042 . . . . . . . . . 10  |-  ( ( ( card `  A
)  e.  om  /\  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) )  e.  om )  ->  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) )  e.  om )
3627, 3, 35sylancl 662 . . . . . . . . 9  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( card `  A )  +o  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) )  e. 
om )
37 f1ocnvfv1 5978 . . . . . . . . 9  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0  /\  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) )  e.  om )  ->  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) ) )  =  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) )
3834, 36, 37sylancr 663 . . . . . . . 8  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) ) )  =  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) )
39 ficardom 8123 . . . . . . . . . 10  |-  ( B  e.  Fin  ->  ( card `  B )  e. 
om )
4039ad2antlr 726 . . . . . . . . 9  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( card `  B )  e. 
om )
41 f1ocnvfv1 5978 . . . . . . . . 9  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) : om -1-1-onto-> NN0  /\  ( card `  B
)  e.  om )  ->  ( `' ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  B
) ) )  =  ( card `  B
) )
4234, 40, 41sylancr 663 . . . . . . . 8  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  ( `' ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  B
) ) )  =  ( card `  B
) )
4333, 38, 423eqtr3d 2478 . . . . . . 7  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  (
( card `  A )  +o  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) ) )  =  ( card `  B
) )
44 oveq2 6094 . . . . . . . . 9  |-  ( y  =  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) )  ->  (
( card `  A )  +o  y )  =  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) ) )
4544eqeq1d 2446 . . . . . . . 8  |-  ( y  =  ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) )  ->  (
( ( card `  A
)  +o  y )  =  ( card `  B
)  <->  ( ( card `  A )  +o  ( card `  ( 1 ... ( ( # `  B
)  -  ( # `  A ) ) ) ) )  =  (
card `  B )
) )
4645rspcev 3068 . . . . . . 7  |-  ( ( ( card `  (
1 ... ( ( # `  B )  -  ( # `
 A ) ) ) )  e.  om  /\  ( ( card `  A
)  +o  ( card `  ( 1 ... (
( # `  B )  -  ( # `  A
) ) ) ) )  =  ( card `  B ) )  ->  E. y  e.  om  ( ( card `  A
)  +o  y )  =  ( card `  B
) )
473, 43, 46sylancr 663 . . . . . 6  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( # `  A
)  <_  ( # `  B
) )  ->  E. y  e.  om  ( ( card `  A )  +o  y
)  =  ( card `  B ) )
4847ex 434 . . . . 5  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  <_  ( # `  B
)  ->  E. y  e.  om  ( ( card `  A )  +o  y
)  =  ( card `  B ) ) )
49 cardnn 8125 . . . . . . . . . 10  |-  ( y  e.  om  ->  ( card `  y )  =  y )
5049adantl 466 . . . . . . . . 9  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  om )  ->  ( card `  y
)  =  y )
5150oveq2d 6102 . . . . . . . 8  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  om )  ->  ( ( card `  A )  +o  ( card `  y ) )  =  ( ( card `  A )  +o  y
) )
5251eqeq1d 2446 . . . . . . 7  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  om )  ->  ( ( (
card `  A )  +o  ( card `  y
) )  =  (
card `  B )  <->  ( ( card `  A
)  +o  y )  =  ( card `  B
) ) )
53 fveq2 5686 . . . . . . . 8  |-  ( ( ( card `  A
)  +o  ( card `  y ) )  =  ( card `  B
)  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  y ) ) )  =  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  B
) ) )
54 nnfi 7495 . . . . . . . . 9  |-  ( y  e.  om  ->  y  e.  Fin )
55 ficardom 8123 . . . . . . . . . . . . . 14  |-  ( y  e.  Fin  ->  ( card `  y )  e. 
om )
564hashgadd 12132 . . . . . . . . . . . . . 14  |-  ( ( ( card `  A
)  e.  om  /\  ( card `  y )  e.  om )  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  (
( card `  A )  +o  ( card `  y
) ) )  =  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  A
) )  +  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  y ) ) ) )
5726, 55, 56syl2an 477 . . . . . . . . . . . . 13  |-  ( ( A  e.  Fin  /\  y  e.  Fin )  ->  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  y ) ) )  =  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  A ) )  +  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  y
) ) ) )
584hashgval 12098 . . . . . . . . . . . . . 14  |-  ( y  e.  Fin  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  y ) )  =  ( # `  y
) )
595, 58oveqan12d 6105 . . . . . . . . . . . . 13  |-  ( ( A  e.  Fin  /\  y  e.  Fin )  ->  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  A
) )  +  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( card `  y ) ) )  =  ( (
# `  A )  +  ( # `  y
) ) )
6057, 59eqtrd 2470 . . . . . . . . . . . 12  |-  ( ( A  e.  Fin  /\  y  e.  Fin )  ->  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  y ) ) )  =  ( ( # `  A )  +  (
# `  y )
) )
6160adantlr 714 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  Fin )  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( ( card `  A
)  +o  ( card `  y ) ) )  =  ( ( # `  A )  +  (
# `  y )
) )
6230ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  Fin )  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  0 )  |`  om ) `  ( card `  B
) )  =  (
# `  B )
)
6361, 62eqeq12d 2452 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  Fin )  ->  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( (
card `  A )  +o  ( card `  y
) ) )  =  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  B
) )  <->  ( ( # `
 A )  +  ( # `  y
) )  =  (
# `  B )
) )
64 hashcl 12118 . . . . . . . . . . . . . . 15  |-  ( y  e.  Fin  ->  ( # `
 y )  e. 
NN0 )
6564nn0ge0d 10631 . . . . . . . . . . . . . 14  |-  ( y  e.  Fin  ->  0  <_  ( # `  y
) )
6665adantl 466 . . . . . . . . . . . . 13  |-  ( ( A  e.  Fin  /\  y  e.  Fin )  ->  0  <_  ( # `  y
) )
679nn0red 10629 . . . . . . . . . . . . . 14  |-  ( A  e.  Fin  ->  ( # `
 A )  e.  RR )
6864nn0red 10629 . . . . . . . . . . . . . 14  |-  ( y  e.  Fin  ->  ( # `
 y )  e.  RR )
69 addge01 9841 . . . . . . . . . . . . . 14  |-  ( ( ( # `  A
)  e.  RR  /\  ( # `  y )  e.  RR )  -> 
( 0  <_  ( # `
 y )  <->  ( # `  A
)  <_  ( ( # `
 A )  +  ( # `  y
) ) ) )
7067, 68, 69syl2an 477 . . . . . . . . . . . . 13  |-  ( ( A  e.  Fin  /\  y  e.  Fin )  ->  ( 0  <_  ( # `
 y )  <->  ( # `  A
)  <_  ( ( # `
 A )  +  ( # `  y
) ) ) )
7166, 70mpbid 210 . . . . . . . . . . . 12  |-  ( ( A  e.  Fin  /\  y  e.  Fin )  ->  ( # `  A
)  <_  ( ( # `
 A )  +  ( # `  y
) ) )
7271adantlr 714 . . . . . . . . . . 11  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  Fin )  ->  ( # `  A
)  <_  ( ( # `
 A )  +  ( # `  y
) ) )
73 breq2 4291 . . . . . . . . . . 11  |-  ( ( ( # `  A
)  +  ( # `  y ) )  =  ( # `  B
)  ->  ( ( # `
 A )  <_ 
( ( # `  A
)  +  ( # `  y ) )  <->  ( # `  A
)  <_  ( # `  B
) ) )
7472, 73syl5ibcom 220 . . . . . . . . . 10  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  Fin )  ->  ( ( (
# `  A )  +  ( # `  y
) )  =  (
# `  B )  ->  ( # `  A
)  <_  ( # `  B
) ) )
7563, 74sylbid 215 . . . . . . . . 9  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  Fin )  ->  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( (
card `  A )  +o  ( card `  y
) ) )  =  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  B
) )  ->  ( # `
 A )  <_ 
( # `  B ) ) )
7654, 75sylan2 474 . . . . . . . 8  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  om )  ->  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  0 )  |`  om ) `  ( (
card `  A )  +o  ( card `  y
) ) )  =  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  0 )  |`  om ) `  ( card `  B
) )  ->  ( # `
 A )  <_ 
( # `  B ) ) )
7753, 76syl5 32 . . . . . . 7  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  om )  ->  ( ( (
card `  A )  +o  ( card `  y
) )  =  (
card `  B )  ->  ( # `  A
)  <_  ( # `  B
) ) )
7852, 77sylbird 235 . . . . . 6  |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  y  e.  om )  ->  ( ( (
card `  A )  +o  y )  =  (
card `  B )  ->  ( # `  A
)  <_  ( # `  B
) ) )
7978rexlimdva 2836 . . . . 5  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( E. y  e. 
om  ( ( card `  A )  +o  y
)  =  ( card `  B )  ->  ( # `
 A )  <_ 
( # `  B ) ) )
8048, 79impbid 191 . . . 4  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  <_  ( # `  B
)  <->  E. y  e.  om  ( ( card `  A
)  +o  y )  =  ( card `  B
) ) )
81 nnawordex 7068 . . . . 5  |-  ( ( ( card `  A
)  e.  om  /\  ( card `  B )  e.  om )  ->  (
( card `  A )  C_  ( card `  B
)  <->  E. y  e.  om  ( ( card `  A
)  +o  y )  =  ( card `  B
) ) )
8226, 39, 81syl2an 477 . . . 4  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( card `  A
)  C_  ( card `  B )  <->  E. y  e.  om  ( ( card `  A )  +o  y
)  =  ( card `  B ) ) )
83 finnum 8110 . . . . 5  |-  ( A  e.  Fin  ->  A  e.  dom  card )
84 finnum 8110 . . . . 5  |-  ( B  e.  Fin  ->  B  e.  dom  card )
85 carddom2 8139 . . . . 5  |-  ( ( A  e.  dom  card  /\  B  e.  dom  card )  ->  ( ( card `  A )  C_  ( card `  B )  <->  A  ~<_  B ) )
8683, 84, 85syl2an 477 . . . 4  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( card `  A
)  C_  ( card `  B )  <->  A  ~<_  B ) )
8780, 82, 863bitr2d 281 . . 3  |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  A
)  <_  ( # `  B
)  <->  A  ~<_  B )
)
8887adantlr 714 . 2  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  B  e.  Fin )  ->  ( ( # `  A )  <_  ( # `
 B )  <->  A  ~<_  B ) )
89 hashxrcl 12119 . . . . . 6  |-  ( A  e.  Fin  ->  ( # `
 A )  e. 
RR* )
9089ad2antrr 725 . . . . 5  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  ( # `
 A )  e. 
RR* )
91 pnfge 11102 . . . . 5  |-  ( (
# `  A )  e.  RR*  ->  ( # `  A
)  <_ +oo )
9290, 91syl 16 . . . 4  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  ( # `
 A )  <_ +oo )
93 hashinf 12100 . . . . 5  |-  ( ( B  e.  V  /\  -.  B  e.  Fin )  ->  ( # `  B
)  = +oo )
9493adantll 713 . . . 4  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  ( # `
 B )  = +oo )
9592, 94breqtrrd 4313 . . 3  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  ( # `
 A )  <_ 
( # `  B ) )
96 isinffi 8154 . . . . . 6  |-  ( ( -.  B  e.  Fin  /\  A  e.  Fin )  ->  E. f  f : A -1-1-> B )
9796ancoms 453 . . . . 5  |-  ( ( A  e.  Fin  /\  -.  B  e.  Fin )  ->  E. f  f : A -1-1-> B )
9897adantlr 714 . . . 4  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  E. f 
f : A -1-1-> B
)
99 brdomg 7312 . . . . 5  |-  ( B  e.  V  ->  ( A  ~<_  B  <->  E. f 
f : A -1-1-> B
) )
10099ad2antlr 726 . . . 4  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  ( A  ~<_  B  <->  E. f 
f : A -1-1-> B
) )
10198, 100mpbird 232 . . 3  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  A  ~<_  B )
10295, 1012thd 240 . 2  |-  ( ( ( A  e.  Fin  /\  B  e.  V )  /\  -.  B  e. 
Fin )  ->  (
( # `  A )  <_  ( # `  B
)  <->  A  ~<_  B )
)
10388, 102pm2.61dan 789 1  |-  ( ( A  e.  Fin  /\  B  e.  V )  ->  ( ( # `  A
)  <_  ( # `  B
)  <->  A  ~<_  B )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   E.wrex 2711   _Vcvv 2967    C_ wss 3323   class class class wbr 4287    e. cmpt 4345   `'ccnv 4834   dom cdm 4835    |` cres 4837   -1-1->wf1 5410   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6086   omcom 6471   reccrdg 6857    +o coa 6909    ~<_ cdom 7300   Fincfn 7302   cardccrd 8097   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277   +oocpnf 9407   RR*cxr 9409    <_ cle 9411    - cmin 9587   NN0cn0 10571   ...cfz 11429   #chash 12095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-n0 10572  df-z 10639  df-uz 10854  df-fz 11430  df-hash 12096
This theorem is referenced by:  hashdomi  12135  hashsdom  12136  hashun2  12138  hashss  12158  hashsslei  12168  hashge3el3dif  12179  hashfun  12191  hashf1  12202  isercoll  13137  phicl2  13835  phibnd  13838  prmreclem2  13970  prmreclem3  13971  4sqlem11  14008  vdwlem11  14044  ramub2  14067  0ram  14073  ram0  14075  sylow1lem4  16091  pgpssslw  16104  fislw  16115  znfld  17968  znidomb  17969  fta1blem  21615  birthdaylem3  22322  basellem4  22396  ppiwordi  22475  musum  22506  ppiub  22518  chpub  22534  lgsqrlem4  22658  umgraex  23208  sizeusglecusg  23345  konigsberg  23559  derangenlem  27011  subfaclefac  27016  erdsze2lem1  27043  snmlff  27170  idomsubgmo  29516
  Copyright terms: Public domain W3C validator