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