Step |
Hyp |
Ref |
Expression |
1 |
|
erdsze.n |
|- ( ph -> N e. NN ) |
2 |
|
erdsze.f |
|- ( ph -> F : ( 1 ... N ) -1-1-> RR ) |
3 |
|
erdszelem.k |
|- K = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) ) |
4 |
|
erdszelem.o |
|- O Or RR |
5 |
|
elfznn |
|- ( A e. ( 1 ... N ) -> A e. NN ) |
6 |
5
|
adantl |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> A e. NN ) |
7 |
|
elfz1end |
|- ( A e. NN <-> A e. ( 1 ... A ) ) |
8 |
6 7
|
sylib |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> A e. ( 1 ... A ) ) |
9 |
8
|
snssd |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> { A } C_ ( 1 ... A ) ) |
10 |
|
elsni |
|- ( x e. { A } -> x = A ) |
11 |
|
elsni |
|- ( y e. { A } -> y = A ) |
12 |
10 11
|
breqan12d |
|- ( ( x e. { A } /\ y e. { A } ) -> ( x < y <-> A < A ) ) |
13 |
12
|
adantl |
|- ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> ( x < y <-> A < A ) ) |
14 |
|
fzssuz |
|- ( 1 ... N ) C_ ( ZZ>= ` 1 ) |
15 |
|
uzssz |
|- ( ZZ>= ` 1 ) C_ ZZ |
16 |
|
zssre |
|- ZZ C_ RR |
17 |
15 16
|
sstri |
|- ( ZZ>= ` 1 ) C_ RR |
18 |
14 17
|
sstri |
|- ( 1 ... N ) C_ RR |
19 |
|
simpr |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> A e. ( 1 ... N ) ) |
20 |
19
|
adantr |
|- ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> A e. ( 1 ... N ) ) |
21 |
18 20
|
sseldi |
|- ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> A e. RR ) |
22 |
21
|
ltnrd |
|- ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> -. A < A ) |
23 |
22
|
pm2.21d |
|- ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> ( A < A -> ( F ` x ) O ( F ` y ) ) ) |
24 |
13 23
|
sylbid |
|- ( ( ( ph /\ A e. ( 1 ... N ) ) /\ ( x e. { A } /\ y e. { A } ) ) -> ( x < y -> ( F ` x ) O ( F ` y ) ) ) |
25 |
24
|
ralrimivva |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) |
26 |
|
f1f |
|- ( F : ( 1 ... N ) -1-1-> RR -> F : ( 1 ... N ) --> RR ) |
27 |
2 26
|
syl |
|- ( ph -> F : ( 1 ... N ) --> RR ) |
28 |
27
|
adantr |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> F : ( 1 ... N ) --> RR ) |
29 |
19
|
snssd |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> { A } C_ ( 1 ... N ) ) |
30 |
|
ltso |
|- < Or RR |
31 |
|
soss |
|- ( ( 1 ... N ) C_ RR -> ( < Or RR -> < Or ( 1 ... N ) ) ) |
32 |
18 30 31
|
mp2 |
|- < Or ( 1 ... N ) |
33 |
|
soisores |
|- ( ( ( < Or ( 1 ... N ) /\ O Or RR ) /\ ( F : ( 1 ... N ) --> RR /\ { A } C_ ( 1 ... N ) ) ) -> ( ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) <-> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) ) |
34 |
32 4 33
|
mpanl12 |
|- ( ( F : ( 1 ... N ) --> RR /\ { A } C_ ( 1 ... N ) ) -> ( ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) <-> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) ) |
35 |
28 29 34
|
syl2anc |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> ( ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) <-> A. x e. { A } A. y e. { A } ( x < y -> ( F ` x ) O ( F ` y ) ) ) ) |
36 |
25 35
|
mpbird |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) ) |
37 |
|
snidg |
|- ( A e. ( 1 ... N ) -> A e. { A } ) |
38 |
37
|
adantl |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> A e. { A } ) |
39 |
|
eqid |
|- { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } |
40 |
39
|
erdszelem1 |
|- ( { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } <-> ( { A } C_ ( 1 ... A ) /\ ( F |` { A } ) Isom < , O ( { A } , ( F " { A } ) ) /\ A e. { A } ) ) |
41 |
9 36 38 40
|
syl3anbrc |
|- ( ( ph /\ A e. ( 1 ... N ) ) -> { A } e. { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) } ) |