Metamath Proof Explorer

Theorem sticksstones4

Description: Equinumerosity lemma for sticks and stones. (Contributed by metakunt, 28-Sep-2024)

Ref Expression
Hypotheses sticksstones4.1 
|- ( ph -> N e. NN0 )
sticksstones4.2 
|- ( ph -> K e. NN0 )
sticksstones4.3 
|- B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K }
sticksstones4.4 
|- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
Assertion sticksstones4 
|- ( ph -> A ~~ B )

Proof

Step Hyp Ref Expression
1 sticksstones4.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones4.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones4.3 
 |-  B = { a e. ~P ( 1 ... N ) | ( # ` a ) = K }
4 sticksstones4.4 
 |-  A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
5 eqid 
 |-  ( p e. A |-> ran p ) = ( p e. A |-> ran p )
6 1 2 3 4 5 sticksstones2 
 |-  ( ph -> ( p e. A |-> ran p ) : A -1-1-> B )
7 1 2 3 4 5 sticksstones3 
 |-  ( ph -> ( p e. A |-> ran p ) : A -onto-> B )
8 6 7 jca 
 |-  ( ph -> ( ( p e. A |-> ran p ) : A -1-1-> B /\ ( p e. A |-> ran p ) : A -onto-> B ) )
9 df-f1o 
 |-  ( ( p e. A |-> ran p ) : A -1-1-onto-> B <-> ( ( p e. A |-> ran p ) : A -1-1-> B /\ ( p e. A |-> ran p ) : A -onto-> B ) )
10 8 9 sylibr 
 |-  ( ph -> ( p e. A |-> ran p ) : A -1-1-onto-> B )
11 simpl 
 |-  ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) -> f : ( 1 ... K ) --> ( 1 ... N ) )
12 11 a1i 
 |-  ( ph -> ( ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) -> f : ( 1 ... K ) --> ( 1 ... N ) ) )
13 12 ss2abdv 
 |-  ( ph -> { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } C_ { f | f : ( 1 ... K ) --> ( 1 ... N ) } )
14 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
15 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
16 mapex 
 |-  ( ( ( 1 ... K ) e. Fin /\ ( 1 ... N ) e. Fin ) -> { f | f : ( 1 ... K ) --> ( 1 ... N ) } e. _V )
17 14 15 16 syl2anc 
 |-  ( ph -> { f | f : ( 1 ... K ) --> ( 1 ... N ) } e. _V )
18 ssexg 
 |-  ( ( { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } C_ { f | f : ( 1 ... K ) --> ( 1 ... N ) } /\ { f | f : ( 1 ... K ) --> ( 1 ... N ) } e. _V ) -> { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } e. _V )
19 13 17 18 syl2anc 
 |-  ( ph -> { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } e. _V )
20 4 eleq1i 
 |-  ( A e. _V <-> { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } e. _V )
21 19 20 sylibr 
 |-  ( ph -> A e. _V )
22 21 mptexd 
 |-  ( ph -> ( p e. A |-> ran p ) e. _V )
23 f1oeq1 
 |-  ( g = ( p e. A |-> ran p ) -> ( g : A -1-1-onto-> B <-> ( p e. A |-> ran p ) : A -1-1-onto-> B ) )
24 23 biimprd 
 |-  ( g = ( p e. A |-> ran p ) -> ( ( p e. A |-> ran p ) : A -1-1-onto-> B -> g : A -1-1-onto-> B ) )
25 24 adantl 
 |-  ( ( ph /\ g = ( p e. A |-> ran p ) ) -> ( ( p e. A |-> ran p ) : A -1-1-onto-> B -> g : A -1-1-onto-> B ) )
26 22 25 spcimedv 
 |-  ( ph -> ( ( p e. A |-> ran p ) : A -1-1-onto-> B -> E. g g : A -1-1-onto-> B ) )
27 10 26 mpd 
 |-  ( ph -> E. g g : A -1-1-onto-> B )
28 bren 
 |-  ( A ~~ B <-> E. g g : A -1-1-onto-> B )
29 27 28 sylibr 
 |-  ( ph -> A ~~ B )