Metamath Proof Explorer

Theorem erdszelem2

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypothesis erdszelem1.1 
|- S = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) }
Assertion erdszelem2 
|- ( ( # " S ) e. Fin /\ ( # " S ) C_ NN )

Proof

Step Hyp Ref Expression
1 erdszelem1.1 
 |-  S = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) }
2 fzfi 
 |-  ( 1 ... A ) e. Fin
3 pwfi 
 |-  ( ( 1 ... A ) e. Fin <-> ~P ( 1 ... A ) e. Fin )
4 2 3 mpbi 
 |-  ~P ( 1 ... A ) e. Fin
5 ssrab2 
 |-  { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } C_ ~P ( 1 ... A )
6 1 5 eqsstri 
 |-  S C_ ~P ( 1 ... A )
7 ssfi 
 |-  ( ( ~P ( 1 ... A ) e. Fin /\ S C_ ~P ( 1 ... A ) ) -> S e. Fin )
8 4 6 7 mp2an 
 |-  S e. Fin
9 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
10 ffun 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> Fun # )
11 9 10 ax-mp 
 |-  Fun #
12 ssv 
 |-  S C_ _V
13 9 fdmi 
 |-  dom # = _V
14 12 13 sseqtrri 
 |-  S C_ dom #
15 fores 
 |-  ( ( Fun # /\ S C_ dom # ) -> ( # |` S ) : S -onto-> ( # " S ) )
16 11 14 15 mp2an 
 |-  ( # |` S ) : S -onto-> ( # " S )
17 fofi 
 |-  ( ( S e. Fin /\ ( # |` S ) : S -onto-> ( # " S ) ) -> ( # " S ) e. Fin )
18 8 16 17 mp2an 
 |-  ( # " S ) e. Fin
19 funimass4 
 |-  ( ( Fun # /\ S C_ dom # ) -> ( ( # " S ) C_ NN <-> A. x e. S ( # ` x ) e. NN ) )
20 11 14 19 mp2an 
 |-  ( ( # " S ) C_ NN <-> A. x e. S ( # ` x ) e. NN )
21 1 erdszelem1 
 |-  ( x e. S <-> ( x C_ ( 1 ... A ) /\ ( F |` x ) Isom < , O ( x , ( F " x ) ) /\ A e. x ) )
22 ne0i 
 |-  ( A e. x -> x =/= (/) )
23 22 3ad2ant3 
 |-  ( ( x C_ ( 1 ... A ) /\ ( F |` x ) Isom < , O ( x , ( F " x ) ) /\ A e. x ) -> x =/= (/) )
24 simp1 
 |-  ( ( x C_ ( 1 ... A ) /\ ( F |` x ) Isom < , O ( x , ( F " x ) ) /\ A e. x ) -> x C_ ( 1 ... A ) )
25 ssfi 
 |-  ( ( ( 1 ... A ) e. Fin /\ x C_ ( 1 ... A ) ) -> x e. Fin )
26 2 24 25 sylancr 
 |-  ( ( x C_ ( 1 ... A ) /\ ( F |` x ) Isom < , O ( x , ( F " x ) ) /\ A e. x ) -> x e. Fin )
27 hashnncl 
 |-  ( x e. Fin -> ( ( # ` x ) e. NN <-> x =/= (/) ) )
28 26 27 syl 
 |-  ( ( x C_ ( 1 ... A ) /\ ( F |` x ) Isom < , O ( x , ( F " x ) ) /\ A e. x ) -> ( ( # ` x ) e. NN <-> x =/= (/) ) )
29 23 28 mpbird 
 |-  ( ( x C_ ( 1 ... A ) /\ ( F |` x ) Isom < , O ( x , ( F " x ) ) /\ A e. x ) -> ( # ` x ) e. NN )
30 21 29 sylbi 
 |-  ( x e. S -> ( # ` x ) e. NN )
31 20 30 mprgbir 
 |-  ( # " S ) C_ NN
32 18 31 pm3.2i 
 |-  ( ( # " S ) e. Fin /\ ( # " S ) C_ NN )