Metamath Proof Explorer

Theorem erdszelem10

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

Ref Expression
Hypotheses erdsze.n 
|- ( ph -> N e. NN )
erdsze.f 
|- ( ph -> F : ( 1 ... N ) -1-1-> RR )
erdszelem.i 
|- I = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
erdszelem.j 
|- J = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
erdszelem.t 
|- T = ( n e. ( 1 ... N ) |-> <. ( I ` n ) , ( J ` n ) >. )
erdszelem.r 
|- ( ph -> R e. NN )
erdszelem.s 
|- ( ph -> S e. NN )
erdszelem.m 
|- ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N )
Assertion erdszelem10 
|- ( ph -> E. m e. ( 1 ... N ) ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 erdsze.n 
 |-  ( ph -> N e. NN )
2 erdsze.f 
 |-  ( ph -> F : ( 1 ... N ) -1-1-> RR )
3 erdszelem.i 
 |-  I = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
4 erdszelem.j 
 |-  J = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) )
5 erdszelem.t 
 |-  T = ( n e. ( 1 ... N ) |-> <. ( I ` n ) , ( J ` n ) >. )
6 erdszelem.r 
 |-  ( ph -> R e. NN )
7 erdszelem.s 
 |-  ( ph -> S e. NN )
8 erdszelem.m 
 |-  ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N )
9 fzfi 
 |-  ( 1 ... ( R - 1 ) ) e. Fin
10 fzfi 
 |-  ( 1 ... ( S - 1 ) ) e. Fin
11 xpfi 
 |-  ( ( ( 1 ... ( R - 1 ) ) e. Fin /\ ( 1 ... ( S - 1 ) ) e. Fin ) -> ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) e. Fin )
12 9 10 11 mp2an 
 |-  ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) e. Fin
13 ssdomg 
 |-  ( ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) e. Fin -> ( ran T C_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) -> ran T ~<_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
14 12 13 ax-mp 
 |-  ( ran T C_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) -> ran T ~<_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) )
15 domnsym 
 |-  ( ran T ~<_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) -> -. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ran T )
16 14 15 syl 
 |-  ( ran T C_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) -> -. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ran T )
17 hashxp 
 |-  ( ( ( 1 ... ( R - 1 ) ) e. Fin /\ ( 1 ... ( S - 1 ) ) e. Fin ) -> ( # ` ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) = ( ( # ` ( 1 ... ( R - 1 ) ) ) x. ( # ` ( 1 ... ( S - 1 ) ) ) ) )
18 9 10 17 mp2an 
 |-  ( # ` ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) = ( ( # ` ( 1 ... ( R - 1 ) ) ) x. ( # ` ( 1 ... ( S - 1 ) ) ) )
19 nnm1nn0 
 |-  ( R e. NN -> ( R - 1 ) e. NN0 )
20 hashfz1 
 |-  ( ( R - 1 ) e. NN0 -> ( # ` ( 1 ... ( R - 1 ) ) ) = ( R - 1 ) )
21 6 19 20 3syl 
 |-  ( ph -> ( # ` ( 1 ... ( R - 1 ) ) ) = ( R - 1 ) )
22 nnm1nn0 
 |-  ( S e. NN -> ( S - 1 ) e. NN0 )
23 hashfz1 
 |-  ( ( S - 1 ) e. NN0 -> ( # ` ( 1 ... ( S - 1 ) ) ) = ( S - 1 ) )
24 7 22 23 3syl 
 |-  ( ph -> ( # ` ( 1 ... ( S - 1 ) ) ) = ( S - 1 ) )
25 21 24 oveq12d 
 |-  ( ph -> ( ( # ` ( 1 ... ( R - 1 ) ) ) x. ( # ` ( 1 ... ( S - 1 ) ) ) ) = ( ( R - 1 ) x. ( S - 1 ) ) )
26 18 25 eqtrid 
 |-  ( ph -> ( # ` ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) = ( ( R - 1 ) x. ( S - 1 ) ) )
27 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
28 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
29 27 28 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
30 8 26 29 3brtr4d 
 |-  ( ph -> ( # ` ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) < ( # ` ( 1 ... N ) ) )
31 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
32 hashsdom 
 |-  ( ( ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) < ( # ` ( 1 ... N ) ) <-> ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ( 1 ... N ) ) )
33 12 31 32 sylancr 
 |-  ( ph -> ( ( # ` ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) < ( # ` ( 1 ... N ) ) <-> ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ( 1 ... N ) ) )
34 30 33 mpbid 
 |-  ( ph -> ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ( 1 ... N ) )
35 1 2 3 4 5 erdszelem9 
 |-  ( ph -> T : ( 1 ... N ) -1-1-> ( NN X. NN ) )
36 f1f1orn 
 |-  ( T : ( 1 ... N ) -1-1-> ( NN X. NN ) -> T : ( 1 ... N ) -1-1-onto-> ran T )
37 ovex 
 |-  ( 1 ... N ) e. _V
38 37 f1oen 
 |-  ( T : ( 1 ... N ) -1-1-onto-> ran T -> ( 1 ... N ) ~~ ran T )
39 35 36 38 3syl 
 |-  ( ph -> ( 1 ... N ) ~~ ran T )
40 sdomentr 
 |-  ( ( ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ( 1 ... N ) /\ ( 1 ... N ) ~~ ran T ) -> ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ran T )
41 34 39 40 syl2anc 
 |-  ( ph -> ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ~< ran T )
42 16 41 nsyl3 
 |-  ( ph -> -. ran T C_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) )
43 nss 
 |-  ( -. ran T C_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> E. s ( s e. ran T /\ -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
44 df-rex 
 |-  ( E. s e. ran T -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> E. s ( s e. ran T /\ -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
45 43 44 bitr4i 
 |-  ( -. ran T C_ ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> E. s e. ran T -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) )
46 42 45 sylib 
 |-  ( ph -> E. s e. ran T -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) )
47 f1fn 
 |-  ( T : ( 1 ... N ) -1-1-> ( NN X. NN ) -> T Fn ( 1 ... N ) )
48 eleq1 
 |-  ( s = ( T ` m ) -> ( s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
49 48 notbid 
 |-  ( s = ( T ` m ) -> ( -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
50 49 rexrn 
 |-  ( T Fn ( 1 ... N ) -> ( E. s e. ran T -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> E. m e. ( 1 ... N ) -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
51 35 47 50 3syl 
 |-  ( ph -> ( E. s e. ran T -. s e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> E. m e. ( 1 ... N ) -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
52 46 51 mpbid 
 |-  ( ph -> E. m e. ( 1 ... N ) -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) )
53 fveq2 
 |-  ( n = m -> ( I ` n ) = ( I ` m ) )
54 fveq2 
 |-  ( n = m -> ( J ` n ) = ( J ` m ) )
55 53 54 opeq12d 
 |-  ( n = m -> <. ( I ` n ) , ( J ` n ) >. = <. ( I ` m ) , ( J ` m ) >. )
56 opex 
 |-  <. ( I ` m ) , ( J ` m ) >. e. _V
57 55 5 56 fvmpt 
 |-  ( m e. ( 1 ... N ) -> ( T ` m ) = <. ( I ` m ) , ( J ` m ) >. )
58 57 adantl 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( T ` m ) = <. ( I ` m ) , ( J ` m ) >. )
59 58 eleq1d 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> <. ( I ` m ) , ( J ` m ) >. e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) ) )
60 opelxp 
 |-  ( <. ( I ` m ) , ( J ` m ) >. e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> ( ( I ` m ) e. ( 1 ... ( R - 1 ) ) /\ ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) )
61 59 60 bitrdi 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> ( ( I ` m ) e. ( 1 ... ( R - 1 ) ) /\ ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) )
62 61 notbid 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> -. ( ( I ` m ) e. ( 1 ... ( R - 1 ) ) /\ ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) )
63 ianor 
 |-  ( -. ( ( I ` m ) e. ( 1 ... ( R - 1 ) ) /\ ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) <-> ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) )
64 62 63 bitrdi 
 |-  ( ( ph /\ m e. ( 1 ... N ) ) -> ( -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) )
65 64 rexbidva 
 |-  ( ph -> ( E. m e. ( 1 ... N ) -. ( T ` m ) e. ( ( 1 ... ( R - 1 ) ) X. ( 1 ... ( S - 1 ) ) ) <-> E. m e. ( 1 ... N ) ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) ) )
66 52 65 mpbid 
 |-  ( ph -> E. m e. ( 1 ... N ) ( -. ( I ` m ) e. ( 1 ... ( R - 1 ) ) \/ -. ( J ` m ) e. ( 1 ... ( S - 1 ) ) ) )