Metamath Proof Explorer

Theorem erdsze2lem1

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

Ref Expression
Hypotheses erdsze2.r 
|- ( ph -> R e. NN )
erdsze2.s 
|- ( ph -> S e. NN )
erdsze2.f 
|- ( ph -> F : A -1-1-> RR )
erdsze2.a 
|- ( ph -> A C_ RR )
erdsze2lem.n 
|- N = ( ( R - 1 ) x. ( S - 1 ) )
erdsze2lem.l 
|- ( ph -> N < ( # ` A ) )
Assertion erdsze2lem1 
|- ( ph -> E. f ( f : ( 1 ... ( N + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) )

Proof

Step Hyp Ref Expression
1 erdsze2.r 
 |-  ( ph -> R e. NN )
2 erdsze2.s 
 |-  ( ph -> S e. NN )
3 erdsze2.f 
 |-  ( ph -> F : A -1-1-> RR )
4 erdsze2.a 
 |-  ( ph -> A C_ RR )
5 erdsze2lem.n 
 |-  N = ( ( R - 1 ) x. ( S - 1 ) )
6 erdsze2lem.l 
 |-  ( ph -> N < ( # ` A ) )
7 nnm1nn0 
 |-  ( R e. NN -> ( R - 1 ) e. NN0 )
8 1 7 syl 
 |-  ( ph -> ( R - 1 ) e. NN0 )
9 nnm1nn0 
 |-  ( S e. NN -> ( S - 1 ) e. NN0 )
10 2 9 syl 
 |-  ( ph -> ( S - 1 ) e. NN0 )
11 8 10 nn0mulcld 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) e. NN0 )
12 5 11 eqeltrid 
 |-  ( ph -> N e. NN0 )
13 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
14 hashfz1 
 |-  ( ( N + 1 ) e. NN0 -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
15 12 13 14 3syl 
 |-  ( ph -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
16 15 adantr 
 |-  ( ( ph /\ A e. Fin ) -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
17 6 adantr 
 |-  ( ( ph /\ A e. Fin ) -> N < ( # ` A ) )
18 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
19 nn0ltp1le 
 |-  ( ( N e. NN0 /\ ( # ` A ) e. NN0 ) -> ( N < ( # ` A ) <-> ( N + 1 ) <_ ( # ` A ) ) )
20 12 18 19 syl2an 
 |-  ( ( ph /\ A e. Fin ) -> ( N < ( # ` A ) <-> ( N + 1 ) <_ ( # ` A ) ) )
21 17 20 mpbid 
 |-  ( ( ph /\ A e. Fin ) -> ( N + 1 ) <_ ( # ` A ) )
22 16 21 eqbrtrd 
 |-  ( ( ph /\ A e. Fin ) -> ( # ` ( 1 ... ( N + 1 ) ) ) <_ ( # ` A ) )
23 fzfid 
 |-  ( ( ph /\ A e. Fin ) -> ( 1 ... ( N + 1 ) ) e. Fin )
24 simpr 
 |-  ( ( ph /\ A e. Fin ) -> A e. Fin )
25 hashdom 
 |-  ( ( ( 1 ... ( N + 1 ) ) e. Fin /\ A e. Fin ) -> ( ( # ` ( 1 ... ( N + 1 ) ) ) <_ ( # ` A ) <-> ( 1 ... ( N + 1 ) ) ~<_ A ) )
26 23 24 25 syl2anc 
 |-  ( ( ph /\ A e. Fin ) -> ( ( # ` ( 1 ... ( N + 1 ) ) ) <_ ( # ` A ) <-> ( 1 ... ( N + 1 ) ) ~<_ A ) )
27 22 26 mpbid 
 |-  ( ( ph /\ A e. Fin ) -> ( 1 ... ( N + 1 ) ) ~<_ A )
28 simpr 
 |-  ( ( ph /\ -. A e. Fin ) -> -. A e. Fin )
29 fzfid 
 |-  ( ( ph /\ -. A e. Fin ) -> ( 1 ... ( N + 1 ) ) e. Fin )
30 isinffi 
 |-  ( ( -. A e. Fin /\ ( 1 ... ( N + 1 ) ) e. Fin ) -> E. f f : ( 1 ... ( N + 1 ) ) -1-1-> A )
31 28 29 30 syl2anc 
 |-  ( ( ph /\ -. A e. Fin ) -> E. f f : ( 1 ... ( N + 1 ) ) -1-1-> A )
32 reex 
 |-  RR e. _V
33 ssexg 
 |-  ( ( A C_ RR /\ RR e. _V ) -> A e. _V )
34 4 32 33 sylancl 
 |-  ( ph -> A e. _V )
35 34 adantr 
 |-  ( ( ph /\ -. A e. Fin ) -> A e. _V )
36 brdomg 
 |-  ( A e. _V -> ( ( 1 ... ( N + 1 ) ) ~<_ A <-> E. f f : ( 1 ... ( N + 1 ) ) -1-1-> A ) )
37 35 36 syl 
 |-  ( ( ph /\ -. A e. Fin ) -> ( ( 1 ... ( N + 1 ) ) ~<_ A <-> E. f f : ( 1 ... ( N + 1 ) ) -1-1-> A ) )
38 31 37 mpbird 
 |-  ( ( ph /\ -. A e. Fin ) -> ( 1 ... ( N + 1 ) ) ~<_ A )
39 27 38 pm2.61dan 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) ~<_ A )
40 domeng 
 |-  ( A e. _V -> ( ( 1 ... ( N + 1 ) ) ~<_ A <-> E. s ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) )
41 34 40 syl 
 |-  ( ph -> ( ( 1 ... ( N + 1 ) ) ~<_ A <-> E. s ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) )
42 39 41 mpbid 
 |-  ( ph -> E. s ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) )
43 simprr 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> s C_ A )
44 4 adantr 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> A C_ RR )
45 43 44 sstrd 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> s C_ RR )
46 ltso 
 |-  < Or RR
47 soss 
 |-  ( s C_ RR -> ( < Or RR -> < Or s ) )
48 45 46 47 mpisyl 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> < Or s )
49 fzfid 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( 1 ... ( N + 1 ) ) e. Fin )
50 simprl 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( 1 ... ( N + 1 ) ) ~~ s )
51 enfi 
 |-  ( ( 1 ... ( N + 1 ) ) ~~ s -> ( ( 1 ... ( N + 1 ) ) e. Fin <-> s e. Fin ) )
52 50 51 syl 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( ( 1 ... ( N + 1 ) ) e. Fin <-> s e. Fin ) )
53 49 52 mpbid 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> s e. Fin )
54 fz1iso 
 |-  ( ( < Or s /\ s e. Fin ) -> E. f f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) )
55 48 53 54 syl2anc 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> E. f f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) )
56 isof1o 
 |-  ( f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) -> f : ( 1 ... ( # ` s ) ) -1-1-onto-> s )
57 56 adantl 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f : ( 1 ... ( # ` s ) ) -1-1-onto-> s )
58 hashen 
 |-  ( ( ( 1 ... ( N + 1 ) ) e. Fin /\ s e. Fin ) -> ( ( # ` ( 1 ... ( N + 1 ) ) ) = ( # ` s ) <-> ( 1 ... ( N + 1 ) ) ~~ s ) )
59 49 53 58 syl2anc 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( ( # ` ( 1 ... ( N + 1 ) ) ) = ( # ` s ) <-> ( 1 ... ( N + 1 ) ) ~~ s ) )
60 50 59 mpbird 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( # ` s ) )
61 15 adantr 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( # ` ( 1 ... ( N + 1 ) ) ) = ( N + 1 ) )
62 60 61 eqtr3d 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( # ` s ) = ( N + 1 ) )
63 62 adantr 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> ( # ` s ) = ( N + 1 ) )
64 63 oveq2d 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> ( 1 ... ( # ` s ) ) = ( 1 ... ( N + 1 ) ) )
65 64 f1oeq2d 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> ( f : ( 1 ... ( # ` s ) ) -1-1-onto-> s <-> f : ( 1 ... ( N + 1 ) ) -1-1-onto-> s ) )
66 57 65 mpbid 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f : ( 1 ... ( N + 1 ) ) -1-1-onto-> s )
67 f1of1 
 |-  ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> s -> f : ( 1 ... ( N + 1 ) ) -1-1-> s )
68 66 67 syl 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f : ( 1 ... ( N + 1 ) ) -1-1-> s )
69 simplrr 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> s C_ A )
70 f1ss 
 |-  ( ( f : ( 1 ... ( N + 1 ) ) -1-1-> s /\ s C_ A ) -> f : ( 1 ... ( N + 1 ) ) -1-1-> A )
71 68 69 70 syl2anc 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f : ( 1 ... ( N + 1 ) ) -1-1-> A )
72 simpr 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) )
73 f1ofo 
 |-  ( f : ( 1 ... ( # ` s ) ) -1-1-onto-> s -> f : ( 1 ... ( # ` s ) ) -onto-> s )
74 forn 
 |-  ( f : ( 1 ... ( # ` s ) ) -onto-> s -> ran f = s )
75 isoeq5 
 |-  ( ran f = s -> ( f Isom < , < ( ( 1 ... ( # ` s ) ) , ran f ) <-> f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) )
76 57 73 74 75 4syl 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> ( f Isom < , < ( ( 1 ... ( # ` s ) ) , ran f ) <-> f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) )
77 72 76 mpbird 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f Isom < , < ( ( 1 ... ( # ` s ) ) , ran f ) )
78 isoeq4 
 |-  ( ( 1 ... ( # ` s ) ) = ( 1 ... ( N + 1 ) ) -> ( f Isom < , < ( ( 1 ... ( # ` s ) ) , ran f ) <-> f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) )
79 64 78 syl 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> ( f Isom < , < ( ( 1 ... ( # ` s ) ) , ran f ) <-> f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) )
80 77 79 mpbid 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) )
81 71 80 jca 
 |-  ( ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) /\ f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) ) -> ( f : ( 1 ... ( N + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) )
82 81 ex 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) -> ( f : ( 1 ... ( N + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) ) )
83 82 eximdv 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> ( E. f f Isom < , < ( ( 1 ... ( # ` s ) ) , s ) -> E. f ( f : ( 1 ... ( N + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) ) )
84 55 83 mpd 
 |-  ( ( ph /\ ( ( 1 ... ( N + 1 ) ) ~~ s /\ s C_ A ) ) -> E. f ( f : ( 1 ... ( N + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) )
85 42 84 exlimddv 
 |-  ( ph -> E. f ( f : ( 1 ... ( N + 1 ) ) -1-1-> A /\ f Isom < , < ( ( 1 ... ( N + 1 ) ) , ran f ) ) )