Step |
Hyp |
Ref |
Expression |
1 |
|
erdsze.n |
β’ ( π β π β β ) |
2 |
|
erdsze.f |
β’ ( π β πΉ : ( 1 ... π ) β1-1β β ) |
3 |
|
erdsze.r |
β’ ( π β π
β β ) |
4 |
|
erdsze.s |
β’ ( π β π β β ) |
5 |
|
erdsze.l |
β’ ( π β ( ( π
β 1 ) Β· ( π β 1 ) ) < π ) |
6 |
|
reseq2 |
β’ ( π€ = π¦ β ( πΉ βΎ π€ ) = ( πΉ βΎ π¦ ) ) |
7 |
|
isoeq1 |
β’ ( ( πΉ βΎ π€ ) = ( πΉ βΎ π¦ ) β ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , < ( π€ , ( πΉ β π€ ) ) ) ) |
8 |
6 7
|
syl |
β’ ( π€ = π¦ β ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , < ( π€ , ( πΉ β π€ ) ) ) ) |
9 |
|
isoeq4 |
β’ ( π€ = π¦ β ( ( πΉ βΎ π¦ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π€ ) ) ) ) |
10 |
|
imaeq2 |
β’ ( π€ = π¦ β ( πΉ β π€ ) = ( πΉ β π¦ ) ) |
11 |
|
isoeq5 |
β’ ( ( πΉ β π€ ) = ( πΉ β π¦ ) β ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) ) ) |
12 |
10 11
|
syl |
β’ ( π€ = π¦ β ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) ) ) |
13 |
8 9 12
|
3bitrd |
β’ ( π€ = π¦ β ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) ) ) |
14 |
|
elequ2 |
β’ ( π€ = π¦ β ( π§ β π€ β π§ β π¦ ) ) |
15 |
13 14
|
anbi12d |
β’ ( π€ = π¦ β ( ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) β ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) ) ) |
16 |
15
|
cbvrabv |
β’ { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } = { π¦ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) } |
17 |
|
oveq2 |
β’ ( π§ = π₯ β ( 1 ... π§ ) = ( 1 ... π₯ ) ) |
18 |
17
|
pweqd |
β’ ( π§ = π₯ β π« ( 1 ... π§ ) = π« ( 1 ... π₯ ) ) |
19 |
|
elequ1 |
β’ ( π§ = π₯ β ( π§ β π¦ β π₯ β π¦ ) ) |
20 |
19
|
anbi2d |
β’ ( π§ = π₯ β ( ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) β ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) ) ) |
21 |
18 20
|
rabeqbidv |
β’ ( π§ = π₯ β { π¦ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) } = { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) |
22 |
16 21
|
eqtrid |
β’ ( π§ = π₯ β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } = { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) |
23 |
22
|
imaeq2d |
β’ ( π§ = π₯ β ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) = ( β― β { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) ) |
24 |
23
|
supeq1d |
β’ ( π§ = π₯ β sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) = sup ( ( β― β { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) , β , < ) ) |
25 |
24
|
cbvmptv |
β’ ( π§ β ( 1 ... π ) β¦ sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) ) = ( π₯ β ( 1 ... π ) β¦ sup ( ( β― β { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) , β , < ) ) |
26 |
|
isoeq1 |
β’ ( ( πΉ βΎ π€ ) = ( πΉ βΎ π¦ ) β ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) ) ) |
27 |
6 26
|
syl |
β’ ( π€ = π¦ β ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) ) ) |
28 |
|
isoeq4 |
β’ ( π€ = π¦ β ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π€ ) ) ) ) |
29 |
|
isoeq5 |
β’ ( ( πΉ β π€ ) = ( πΉ β π¦ ) β ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) ) ) |
30 |
10 29
|
syl |
β’ ( π€ = π¦ β ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) ) ) |
31 |
27 28 30
|
3bitrd |
β’ ( π€ = π¦ β ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) ) ) |
32 |
31 14
|
anbi12d |
β’ ( π€ = π¦ β ( ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) β ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) ) ) |
33 |
32
|
cbvrabv |
β’ { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } = { π¦ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) } |
34 |
19
|
anbi2d |
β’ ( π§ = π₯ β ( ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) β ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) ) ) |
35 |
18 34
|
rabeqbidv |
β’ ( π§ = π₯ β { π¦ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π§ β π¦ ) } = { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) |
36 |
33 35
|
eqtrid |
β’ ( π§ = π₯ β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } = { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) |
37 |
36
|
imaeq2d |
β’ ( π§ = π₯ β ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) = ( β― β { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) ) |
38 |
37
|
supeq1d |
β’ ( π§ = π₯ β sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) = sup ( ( β― β { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) , β , < ) ) |
39 |
38
|
cbvmptv |
β’ ( π§ β ( 1 ... π ) β¦ sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) ) = ( π₯ β ( 1 ... π ) β¦ sup ( ( β― β { π¦ β π« ( 1 ... π₯ ) β£ ( ( πΉ βΎ π¦ ) Isom < , β‘ < ( π¦ , ( πΉ β π¦ ) ) β§ π₯ β π¦ ) } ) , β , < ) ) |
40 |
|
eqid |
β’ ( π β ( 1 ... π ) β¦ β¨ ( ( π§ β ( 1 ... π ) β¦ sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) ) β π ) , ( ( π§ β ( 1 ... π ) β¦ sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) ) β π ) β© ) = ( π β ( 1 ... π ) β¦ β¨ ( ( π§ β ( 1 ... π ) β¦ sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) ) β π ) , ( ( π§ β ( 1 ... π ) β¦ sup ( ( β― β { π€ β π« ( 1 ... π§ ) β£ ( ( πΉ βΎ π€ ) Isom < , β‘ < ( π€ , ( πΉ β π€ ) ) β§ π§ β π€ ) } ) , β , < ) ) β π ) β© ) |
41 |
1 2 25 39 40 3 4 5
|
erdszelem11 |
β’ ( π β β π β π« ( 1 ... π ) ( ( π
β€ ( β― β π ) β§ ( πΉ βΎ π ) Isom < , < ( π , ( πΉ β π ) ) ) β¨ ( π β€ ( β― β π ) β§ ( πΉ βΎ π ) Isom < , β‘ < ( π , ( πΉ β π ) ) ) ) ) |