Step |
Hyp |
Ref |
Expression |
1 |
|
erdsze.n |
|- ( ph -> N e. NN ) |
2 |
|
erdsze.f |
|- ( ph -> F : ( 1 ... N ) -1-1-> RR ) |
3 |
|
erdsze.r |
|- ( ph -> R e. NN ) |
4 |
|
erdsze.s |
|- ( ph -> S e. NN ) |
5 |
|
erdsze.l |
|- ( ph -> ( ( R - 1 ) x. ( S - 1 ) ) < N ) |
6 |
|
reseq2 |
|- ( w = y -> ( F |` w ) = ( F |` y ) ) |
7 |
|
isoeq1 |
|- ( ( F |` w ) = ( F |` y ) -> ( ( F |` w ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( w , ( F " w ) ) ) ) |
8 |
6 7
|
syl |
|- ( w = y -> ( ( F |` w ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( w , ( F " w ) ) ) ) |
9 |
|
isoeq4 |
|- ( w = y -> ( ( F |` y ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " w ) ) ) ) |
10 |
|
imaeq2 |
|- ( w = y -> ( F " w ) = ( F " y ) ) |
11 |
|
isoeq5 |
|- ( ( F " w ) = ( F " y ) -> ( ( F |` y ) Isom < , < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " y ) ) ) ) |
12 |
10 11
|
syl |
|- ( w = y -> ( ( F |` y ) Isom < , < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " y ) ) ) ) |
13 |
8 9 12
|
3bitrd |
|- ( w = y -> ( ( F |` w ) Isom < , < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , < ( y , ( F " y ) ) ) ) |
14 |
|
elequ2 |
|- ( w = y -> ( z e. w <-> z e. y ) ) |
15 |
13 14
|
anbi12d |
|- ( w = y -> ( ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) <-> ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) ) ) |
16 |
15
|
cbvrabv |
|- { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) } |
17 |
|
oveq2 |
|- ( z = x -> ( 1 ... z ) = ( 1 ... x ) ) |
18 |
17
|
pweqd |
|- ( z = x -> ~P ( 1 ... z ) = ~P ( 1 ... x ) ) |
19 |
|
elequ1 |
|- ( z = x -> ( z e. y <-> x e. y ) ) |
20 |
19
|
anbi2d |
|- ( z = x -> ( ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) <-> ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) ) ) |
21 |
18 20
|
rabeqbidv |
|- ( z = x -> { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ z e. y ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) |
22 |
16 21
|
eqtrid |
|- ( z = x -> { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) |
23 |
22
|
imaeq2d |
|- ( z = x -> ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) = ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) ) |
24 |
23
|
supeq1d |
|- ( z = x -> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) = sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) ) |
25 |
24
|
cbvmptv |
|- ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) ) |
26 |
|
isoeq1 |
|- ( ( F |` w ) = ( F |` y ) -> ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( w , ( F " w ) ) ) ) |
27 |
6 26
|
syl |
|- ( w = y -> ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( w , ( F " w ) ) ) ) |
28 |
|
isoeq4 |
|- ( w = y -> ( ( F |` y ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " w ) ) ) ) |
29 |
|
isoeq5 |
|- ( ( F " w ) = ( F " y ) -> ( ( F |` y ) Isom < , `' < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " y ) ) ) ) |
30 |
10 29
|
syl |
|- ( w = y -> ( ( F |` y ) Isom < , `' < ( y , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " y ) ) ) ) |
31 |
27 28 30
|
3bitrd |
|- ( w = y -> ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) <-> ( F |` y ) Isom < , `' < ( y , ( F " y ) ) ) ) |
32 |
31 14
|
anbi12d |
|- ( w = y -> ( ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) <-> ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) ) ) |
33 |
32
|
cbvrabv |
|- { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) } |
34 |
19
|
anbi2d |
|- ( z = x -> ( ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) <-> ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) ) ) |
35 |
18 34
|
rabeqbidv |
|- ( z = x -> { y e. ~P ( 1 ... z ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ z e. y ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) |
36 |
33 35
|
eqtrid |
|- ( z = x -> { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } = { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) |
37 |
36
|
imaeq2d |
|- ( z = x -> ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) = ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) ) |
38 |
37
|
supeq1d |
|- ( z = x -> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) = sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) ) |
39 |
38
|
cbvmptv |
|- ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) = ( x e. ( 1 ... N ) |-> sup ( ( # " { y e. ~P ( 1 ... x ) | ( ( F |` y ) Isom < , `' < ( y , ( F " y ) ) /\ x e. y ) } ) , RR , < ) ) |
40 |
|
eqid |
|- ( n e. ( 1 ... N ) |-> <. ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) , ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) >. ) = ( n e. ( 1 ... N ) |-> <. ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) , ( ( z e. ( 1 ... N ) |-> sup ( ( # " { w e. ~P ( 1 ... z ) | ( ( F |` w ) Isom < , `' < ( w , ( F " w ) ) /\ z e. w ) } ) , RR , < ) ) ` n ) >. ) |
41 |
1 2 25 39 40 3 4 5
|
erdszelem11 |
|- ( ph -> E. s e. ~P ( 1 ... N ) ( ( R <_ ( # ` s ) /\ ( F |` s ) Isom < , < ( s , ( F " s ) ) ) \/ ( S <_ ( # ` s ) /\ ( F |` s ) Isom < , `' < ( s , ( F " s ) ) ) ) ) |