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 syl5eq
 |-  ( 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 ) ) ) )