Metamath Proof Explorer

Theorem erdszelem9

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 ) >. )
Assertion erdszelem9 
|- ( ph -> T : ( 1 ... N ) -1-1-> ( NN X. NN ) )

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 ltso 
 |-  < Or RR
7 1 2 3 6 erdszelem6 
 |-  ( ph -> I : ( 1 ... N ) --> NN )
8 7 ffvelrnda 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( I ` n ) e. NN )
9 gtso 
 |-  `' < Or RR
10 1 2 4 9 erdszelem6 
 |-  ( ph -> J : ( 1 ... N ) --> NN )
11 10 ffvelrnda 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( J ` n ) e. NN )
12 opelxpi 
 |-  ( ( ( I ` n ) e. NN /\ ( J ` n ) e. NN ) -> <. ( I ` n ) , ( J ` n ) >. e. ( NN X. NN ) )
13 8 11 12 syl2anc 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> <. ( I ` n ) , ( J ` n ) >. e. ( NN X. NN ) )
14 13 5 fmptd 
 |-  ( ph -> T : ( 1 ... N ) --> ( NN X. NN ) )
15 fveq2 
 |-  ( a = z -> ( T ` a ) = ( T ` z ) )
16 fveq2 
 |-  ( b = w -> ( T ` b ) = ( T ` w ) )
17 15 16 eqeqan12d 
 |-  ( ( a = z /\ b = w ) -> ( ( T ` a ) = ( T ` b ) <-> ( T ` z ) = ( T ` w ) ) )
18 eqeq12 
 |-  ( ( a = z /\ b = w ) -> ( a = b <-> z = w ) )
19 17 18 imbi12d 
 |-  ( ( a = z /\ b = w ) -> ( ( ( T ` a ) = ( T ` b ) -> a = b ) <-> ( ( T ` z ) = ( T ` w ) -> z = w ) ) )
20 fveq2 
 |-  ( a = w -> ( T ` a ) = ( T ` w ) )
21 fveq2 
 |-  ( b = z -> ( T ` b ) = ( T ` z ) )
22 20 21 eqeqan12d 
 |-  ( ( a = w /\ b = z ) -> ( ( T ` a ) = ( T ` b ) <-> ( T ` w ) = ( T ` z ) ) )
23 eqcom 
 |-  ( ( T ` w ) = ( T ` z ) <-> ( T ` z ) = ( T ` w ) )
24 22 23 bitrdi 
 |-  ( ( a = w /\ b = z ) -> ( ( T ` a ) = ( T ` b ) <-> ( T ` z ) = ( T ` w ) ) )
25 eqeq12 
 |-  ( ( a = w /\ b = z ) -> ( a = b <-> w = z ) )
26 eqcom 
 |-  ( w = z <-> z = w )
27 25 26 bitrdi 
 |-  ( ( a = w /\ b = z ) -> ( a = b <-> z = w ) )
28 24 27 imbi12d 
 |-  ( ( a = w /\ b = z ) -> ( ( ( T ` a ) = ( T ` b ) -> a = b ) <-> ( ( T ` z ) = ( T ` w ) -> z = w ) ) )
29 elfzelz 
 |-  ( z e. ( 1 ... N ) -> z e. ZZ )
30 29 zred 
 |-  ( z e. ( 1 ... N ) -> z e. RR )
31 30 ssriv 
 |-  ( 1 ... N ) C_ RR
32 31 a1i 
 |-  ( ph -> ( 1 ... N ) C_ RR )
33 biidd 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) ) ) -> ( ( ( T ` z ) = ( T ` w ) -> z = w ) <-> ( ( T ` z ) = ( T ` w ) -> z = w ) ) )
34 simpr1 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> z e. ( 1 ... N ) )
35 fveq2 
 |-  ( n = z -> ( I ` n ) = ( I ` z ) )
36 fveq2 
 |-  ( n = z -> ( J ` n ) = ( J ` z ) )
37 35 36 opeq12d 
 |-  ( n = z -> <. ( I ` n ) , ( J ` n ) >. = <. ( I ` z ) , ( J ` z ) >. )
38 opex 
 |-  <. ( I ` z ) , ( J ` z ) >. e. _V
39 37 5 38 fvmpt 
 |-  ( z e. ( 1 ... N ) -> ( T ` z ) = <. ( I ` z ) , ( J ` z ) >. )
40 34 39 syl 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( T ` z ) = <. ( I ` z ) , ( J ` z ) >. )
41 simpr2 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> w e. ( 1 ... N ) )
42 fveq2 
 |-  ( n = w -> ( I ` n ) = ( I ` w ) )
43 fveq2 
 |-  ( n = w -> ( J ` n ) = ( J ` w ) )
44 42 43 opeq12d 
 |-  ( n = w -> <. ( I ` n ) , ( J ` n ) >. = <. ( I ` w ) , ( J ` w ) >. )
45 opex 
 |-  <. ( I ` w ) , ( J ` w ) >. e. _V
46 44 5 45 fvmpt 
 |-  ( w e. ( 1 ... N ) -> ( T ` w ) = <. ( I ` w ) , ( J ` w ) >. )
47 41 46 syl 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( T ` w ) = <. ( I ` w ) , ( J ` w ) >. )
48 40 47 eqeq12d 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( T ` z ) = ( T ` w ) <-> <. ( I ` z ) , ( J ` z ) >. = <. ( I ` w ) , ( J ` w ) >. ) )
49 fvex 
 |-  ( I ` z ) e. _V
50 fvex 
 |-  ( J ` z ) e. _V
51 49 50 opth 
 |-  ( <. ( I ` z ) , ( J ` z ) >. = <. ( I ` w ) , ( J ` w ) >. <-> ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) )
52 34 30 syl 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> z e. RR )
53 31 41 sselid 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> w e. RR )
54 simpr3 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> z <_ w )
55 52 53 54 leltned 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( z < w <-> w =/= z ) )
56 2 adantr 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> F : ( 1 ... N ) -1-1-> RR )
57 f1fveq 
 |-  ( ( F : ( 1 ... N ) -1-1-> RR /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) ) ) -> ( ( F ` z ) = ( F ` w ) <-> z = w ) )
58 56 34 41 57 syl12anc 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( F ` z ) = ( F ` w ) <-> z = w ) )
59 58 26 bitr4di 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( F ` z ) = ( F ` w ) <-> w = z ) )
60 59 necon3bid 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( F ` z ) =/= ( F ` w ) <-> w =/= z ) )
61 55 60 bitr4d 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( z < w <-> ( F ` z ) =/= ( F ` w ) ) )
62 61 biimpa 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( F ` z ) =/= ( F ` w ) )
63 f1f 
 |-  ( F : ( 1 ... N ) -1-1-> RR -> F : ( 1 ... N ) --> RR )
64 2 63 syl 
 |-  ( ph -> F : ( 1 ... N ) --> RR )
65 64 ad2antrr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> F : ( 1 ... N ) --> RR )
66 34 adantr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> z e. ( 1 ... N ) )
67 65 66 ffvelrnd 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( F ` z ) e. RR )
68 41 adantr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> w e. ( 1 ... N ) )
69 65 68 ffvelrnd 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( F ` w ) e. RR )
70 67 69 lttri2d 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( ( F ` z ) =/= ( F ` w ) <-> ( ( F ` z ) < ( F ` w ) \/ ( F ` w ) < ( F ` z ) ) ) )
71 62 70 mpbid 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( ( F ` z ) < ( F ` w ) \/ ( F ` w ) < ( F ` z ) ) )
72 1 ad2antrr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> N e. NN )
73 2 ad2antrr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> F : ( 1 ... N ) -1-1-> RR )
74 simpr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> z < w )
75 72 73 3 6 66 68 74 erdszelem8 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( ( I ` z ) = ( I ` w ) -> -. ( F ` z ) < ( F ` w ) ) )
76 72 73 4 9 66 68 74 erdszelem8 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( ( J ` z ) = ( J ` w ) -> -. ( F ` z ) `' < ( F ` w ) ) )
77 75 76 anim12d 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) -> ( -. ( F ` z ) < ( F ` w ) /\ -. ( F ` z ) `' < ( F ` w ) ) ) )
78 ioran 
 |-  ( -. ( ( F ` z ) < ( F ` w ) \/ ( F ` w ) < ( F ` z ) ) <-> ( -. ( F ` z ) < ( F ` w ) /\ -. ( F ` w ) < ( F ` z ) ) )
79 fvex 
 |-  ( F ` z ) e. _V
80 fvex 
 |-  ( F ` w ) e. _V
81 79 80 brcnv 
 |-  ( ( F ` z ) `' < ( F ` w ) <-> ( F ` w ) < ( F ` z ) )
82 81 notbii 
 |-  ( -. ( F ` z ) `' < ( F ` w ) <-> -. ( F ` w ) < ( F ` z ) )
83 82 anbi2i 
 |-  ( ( -. ( F ` z ) < ( F ` w ) /\ -. ( F ` z ) `' < ( F ` w ) ) <-> ( -. ( F ` z ) < ( F ` w ) /\ -. ( F ` w ) < ( F ` z ) ) )
84 78 83 bitr4i 
 |-  ( -. ( ( F ` z ) < ( F ` w ) \/ ( F ` w ) < ( F ` z ) ) <-> ( -. ( F ` z ) < ( F ` w ) /\ -. ( F ` z ) `' < ( F ` w ) ) )
85 77 84 syl6ibr 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> ( ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) -> -. ( ( F ` z ) < ( F ` w ) \/ ( F ` w ) < ( F ` z ) ) ) )
86 71 85 mt2d 
 |-  ( ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) /\ z < w ) -> -. ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) )
87 86 ex 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( z < w -> -. ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) ) )
88 55 87 sylbird 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( w =/= z -> -. ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) ) )
89 88 necon4ad 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( ( I ` z ) = ( I ` w ) /\ ( J ` z ) = ( J ` w ) ) -> w = z ) )
90 51 89 syl5bi 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( <. ( I ` z ) , ( J ` z ) >. = <. ( I ` w ) , ( J ` w ) >. -> w = z ) )
91 48 90 sylbid 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( T ` z ) = ( T ` w ) -> w = z ) )
92 91 26 syl6ib 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) /\ z <_ w ) ) -> ( ( T ` z ) = ( T ` w ) -> z = w ) )
93 19 28 32 33 92 wlogle 
 |-  ( ( ph /\ ( z e. ( 1 ... N ) /\ w e. ( 1 ... N ) ) ) -> ( ( T ` z ) = ( T ` w ) -> z = w ) )
94 93 ralrimivva 
 |-  ( ph -> A. z e. ( 1 ... N ) A. w e. ( 1 ... N ) ( ( T ` z ) = ( T ` w ) -> z = w ) )
95 dff13 
 |-  ( T : ( 1 ... N ) -1-1-> ( NN X. NN ) <-> ( T : ( 1 ... N ) --> ( NN X. NN ) /\ A. z e. ( 1 ... N ) A. w e. ( 1 ... N ) ( ( T ` z ) = ( T ` w ) -> z = w ) ) )
96 14 94 95 sylanbrc 
 |-  ( ph -> T : ( 1 ... N ) -1-1-> ( NN X. NN ) )