Step | Hyp | Ref
| Expression |
1 | | hashf 14244 |
. . . . 5
β’
β―:VβΆ(β0 βͺ {+β}) |
2 | | ffun 6672 |
. . . . 5
β’
(β―:VβΆ(β0 βͺ {+β}) β Fun
β―) |
3 | 1, 2 | ax-mp 5 |
. . . 4
β’ Fun
β― |
4 | | erdszelem.a |
. . . . 5
β’ (π β π΄ β (1...π)) |
5 | | erdsze.n |
. . . . . 6
β’ (π β π β β) |
6 | | erdsze.f |
. . . . . 6
β’ (π β πΉ:(1...π)β1-1ββ) |
7 | | erdszelem.k |
. . . . . 6
β’ πΎ = (π₯ β (1...π) β¦ sup((β― β {π¦ β π« (1...π₯) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π₯ β π¦)}), β, < )) |
8 | | erdszelem.o |
. . . . . 6
β’ π Or β |
9 | 5, 6, 7, 8 | erdszelem5 33846 |
. . . . 5
β’ ((π β§ π΄ β (1...π)) β (πΎβπ΄) β (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)})) |
10 | 4, 9 | mpdan 686 |
. . . 4
β’ (π β (πΎβπ΄) β (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)})) |
11 | | fvelima 6909 |
. . . 4
β’ ((Fun
β― β§ (πΎβπ΄) β (β― β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)})) β βπ β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} (β―βπ) = (πΎβπ΄)) |
12 | 3, 10, 11 | sylancr 588 |
. . 3
β’ (π β βπ β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} (β―βπ) = (πΎβπ΄)) |
13 | | eqid 2733 |
. . . . . 6
β’ {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} = {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} |
14 | 13 | erdszelem1 33842 |
. . . . 5
β’ (π β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} β (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) |
15 | | fzfid 13884 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (1...π΄) β Fin) |
16 | | simplr1 1216 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π β (1...π΄)) |
17 | | ssfi 9120 |
. . . . . . . . . . 11
β’
(((1...π΄) β Fin
β§ π β (1...π΄)) β π β Fin) |
18 | 15, 16, 17 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π β Fin) |
19 | | hashcl 14262 |
. . . . . . . . . 10
β’ (π β Fin β
(β―βπ) β
β0) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β―βπ) β
β0) |
21 | 20 | nn0red 12479 |
. . . . . . . 8
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β―βπ) β β) |
22 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)} = {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)} |
23 | 22 | erdszelem2 33843 |
. . . . . . . . . . . . . 14
β’ ((β―
β {π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β Fin β§ (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β) |
24 | 23 | simpri 487 |
. . . . . . . . . . . . 13
β’ (β―
β {π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β |
25 | | nnssre 12162 |
. . . . . . . . . . . . 13
β’ β
β β |
26 | 24, 25 | sstri 3954 |
. . . . . . . . . . . 12
β’ (β―
β {π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β |
27 | 26 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β) |
28 | 4 | elfzelzd 13448 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β β€) |
29 | | erdszelem.b |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΅ β (1...π)) |
30 | 29 | elfzelzd 13448 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β β€) |
31 | | elfznn 13476 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β (1...π) β π΄ β β) |
32 | 4, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΄ β β) |
33 | 32 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β β) |
34 | | elfznn 13476 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΅ β (1...π) β π΅ β β) |
35 | 29, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π΅ β β) |
36 | 35 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΅ β β) |
37 | | erdszelem.l |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ < π΅) |
38 | 33, 36, 37 | ltled 11308 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β€ π΅) |
39 | | eluz2 12774 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β
(β€β₯βπ΄) β (π΄ β β€ β§ π΅ β β€ β§ π΄ β€ π΅)) |
40 | 28, 30, 38, 39 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β (β€β₯βπ΄)) |
41 | | fzss2 13487 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β
(β€β₯βπ΄) β (1...π΄) β (1...π΅)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π΄) β (1...π΅)) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (1...π΄) β (1...π΅)) |
44 | 16, 43 | sstrd 3955 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π β (1...π΅)) |
45 | | elfz1end 13477 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β β β π΅ β (1...π΅)) |
46 | 35, 45 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΅ β (1...π΅)) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π΅ β (1...π΅)) |
48 | 47 | snssd 4770 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β {π΅} β (1...π΅)) |
49 | 44, 48 | unssd 4147 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (π βͺ {π΅}) β (1...π΅)) |
50 | | simplr2 1217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΉ βΎ π) Isom < , π (π, (πΉ β π))) |
51 | | f1f 6739 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ:(1...π)β1-1ββ β πΉ:(1...π)βΆβ) |
52 | 6, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΉ:(1...π)βΆβ) |
53 | 52 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β πΉ:(1...π)βΆβ) |
54 | | elfzuz3 13444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ β (1...π) β π β (β€β₯βπ΄)) |
55 | | fzss2 13487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(β€β₯βπ΄) β (1...π΄) β (1...π)) |
56 | 4, 54, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π΄) β (1...π)) |
57 | 56 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (1...π΄) β (1...π)) |
58 | 16, 57 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π β (1...π)) |
59 | | fzssuz 13488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(1...π) β
(β€β₯β1) |
60 | | uzssz 12789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(β€β₯β1) β β€ |
61 | | zssre 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ β€
β β |
62 | 60, 61 | sstri 3954 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(β€β₯β1) β β |
63 | 59, 62 | sstri 3954 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(1...π) β
β |
64 | | ltso 11240 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ < Or
β |
65 | | soss 5566 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((1...π) β
β β ( < Or β β < Or (1...π))) |
66 | 63, 64, 65 | mp2 9 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ < Or
(1...π) |
67 | | soisores 7273 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((( <
Or (1...π) β§ π Or β) β§ (πΉ:(1...π)βΆβ β§ π β (1...π))) β ((πΉ βΎ π) Isom < , π (π, (πΉ β π)) β βπ§ β π βπ€ β π (π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
68 | 66, 8, 67 | mpanl12 701 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:(1...π)βΆβ β§ π β (1...π)) β ((πΉ βΎ π) Isom < , π (π, (πΉ β π)) β βπ§ β π βπ€ β π (π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
69 | 53, 58, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((πΉ βΎ π) Isom < , π (π, (πΉ β π)) β βπ§ β π βπ€ β π (π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
70 | 50, 69 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β βπ§ β π βπ€ β π (π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
71 | 70 | r19.21bi 3233 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β βπ€ β π (π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
72 | 16 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π§ β (1...π΄)) |
73 | | elfzle2 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β (1...π΄) β π§ β€ π΄) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π§ β€ π΄) |
75 | 58 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π§ β (1...π)) |
76 | 63, 75 | sselid 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π§ β β) |
77 | 4 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π΄ β (1...π)) |
78 | 77, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π΄ β β) |
79 | 78 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π΄ β β) |
80 | 76, 79 | lenltd 11306 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (π§ β€ π΄ β Β¬ π΄ < π§)) |
81 | 74, 80 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β Β¬ π΄ < π§) |
82 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (πΉ βΎ π) Isom < , π (π, (πΉ β π))) |
83 | | simplr3 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π΄ β π) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π΄ β π) |
85 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π§ β π) |
86 | | isorel 7272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ (π΄ β π β§ π§ β π)) β (π΄ < π§ β ((πΉ βΎ π)βπ΄)π((πΉ βΎ π)βπ§))) |
87 | | fvres 6862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π΄ β π β ((πΉ βΎ π)βπ΄) = (πΉβπ΄)) |
88 | | fvres 6862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ β π β ((πΉ βΎ π)βπ§) = (πΉβπ§)) |
89 | 87, 88 | breqan12d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π΄ β π β§ π§ β π) β (((πΉ βΎ π)βπ΄)π((πΉ βΎ π)βπ§) β (πΉβπ΄)π(πΉβπ§))) |
90 | 89 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ (π΄ β π β§ π§ β π)) β (((πΉ βΎ π)βπ΄)π((πΉ βΎ π)βπ§) β (πΉβπ΄)π(πΉβπ§))) |
91 | 86, 90 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ (π΄ β π β§ π§ β π)) β (π΄ < π§ β (πΉβπ΄)π(πΉβπ§))) |
92 | 82, 84, 85, 91 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (π΄ < π§ β (πΉβπ΄)π(πΉβπ§))) |
93 | 81, 92 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β Β¬ (πΉβπ΄)π(πΉβπ§)) |
94 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (πΉβπ΄)π(πΉβπ΅)) |
95 | 53 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β πΉ:(1...π)βΆβ) |
96 | 95, 75 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (πΉβπ§) β β) |
97 | 95, 77 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (πΉβπ΄) β β) |
98 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π΅ β (1...π)) |
99 | 98 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β π΅ β (1...π)) |
100 | 95, 99 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (πΉβπ΅) β β) |
101 | | sotr2 5578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π Or β β§ ((πΉβπ§) β β β§ (πΉβπ΄) β β β§ (πΉβπ΅) β β)) β ((Β¬ (πΉβπ΄)π(πΉβπ§) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΉβπ§)π(πΉβπ΅))) |
102 | 8, 101 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉβπ§) β β β§ (πΉβπ΄) β β β§ (πΉβπ΅) β β) β ((Β¬ (πΉβπ΄)π(πΉβπ§) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΉβπ§)π(πΉβπ΅))) |
103 | 96, 97, 100, 102 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β ((Β¬ (πΉβπ΄)π(πΉβπ§) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΉβπ§)π(πΉβπ΅))) |
104 | 93, 94, 103 | mp2and 698 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (πΉβπ§)π(πΉβπ΅)) |
105 | 104 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (π§ < π€ β (πΉβπ§)π(πΉβπ΅))) |
106 | | elsni 4604 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β {π΅} β π€ = π΅) |
107 | 106 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β {π΅} β (πΉβπ€) = (πΉβπ΅)) |
108 | 107 | breq2d 5118 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β {π΅} β ((πΉβπ§)π(πΉβπ€) β (πΉβπ§)π(πΉβπ΅))) |
109 | 108 | imbi2d 341 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β {π΅} β ((π§ < π€ β (πΉβπ§)π(πΉβπ€)) β (π§ < π€ β (πΉβπ§)π(πΉβπ΅)))) |
110 | 105, 109 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β (π€ β {π΅} β (π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
111 | 110 | ralrimiv 3139 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β βπ€ β {π΅} (π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
112 | | ralunb 4152 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ€ β
(π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)) β (βπ€ β π (π§ < π€ β (πΉβπ§)π(πΉβπ€)) β§ βπ€ β {π΅} (π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
113 | 71, 111, 112 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π§ β π) β βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
114 | 113 | ralrimiva 3140 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β βπ§ β π βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
115 | 49 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (π βͺ {π΅})) β π€ β (1...π΅)) |
116 | | elfzle2 13451 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π€ β (1...π΅) β π€ β€ π΅) |
117 | 116 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (1...π΅)) β π€ β€ π΅) |
118 | | elfzelz 13447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ β (1...π΅) β π€ β β€) |
119 | 118 | zred 12612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β (1...π΅) β π€ β β) |
120 | 119 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (1...π΅)) β π€ β β) |
121 | 36 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (1...π΅)) β π΅ β β) |
122 | 120, 121 | lenltd 11306 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (1...π΅)) β (π€ β€ π΅ β Β¬ π΅ < π€)) |
123 | 117, 122 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (1...π΅)) β Β¬ π΅ < π€) |
124 | 115, 123 | syldan 592 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (π βͺ {π΅})) β Β¬ π΅ < π€) |
125 | 124 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β§ π€ β (π βͺ {π΅})) β (π΅ < π€ β (πΉβπ§)π(πΉβπ€))) |
126 | 125 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β βπ€ β (π βͺ {π΅})(π΅ < π€ β (πΉβπ§)π(πΉβπ€))) |
127 | | elsni 4604 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π§ β {π΅} β π§ = π΅) |
128 | 127 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β {π΅} β (π§ < π€ β π΅ < π€)) |
129 | 128 | imbi1d 342 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β {π΅} β ((π§ < π€ β (πΉβπ§)π(πΉβπ€)) β (π΅ < π€ β (πΉβπ§)π(πΉβπ€)))) |
130 | 129 | ralbidv 3171 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {π΅} β (βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)) β βπ€ β (π βͺ {π΅})(π΅ < π€ β (πΉβπ§)π(πΉβπ€)))) |
131 | 126, 130 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (π§ β {π΅} β βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
132 | 131 | ralrimiv 3139 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β βπ§ β {π΅}βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
133 | | ralunb 4152 |
. . . . . . . . . . . . . . . 16
β’
(βπ§ β
(π βͺ {π΅})βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)) β (βπ§ β π βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)) β§ βπ§ β {π΅}βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
134 | 114, 132,
133 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β βπ§ β (π βͺ {π΅})βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€))) |
135 | 98 | snssd 4770 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β {π΅} β (1...π)) |
136 | 58, 135 | unssd 4147 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (π βͺ {π΅}) β (1...π)) |
137 | | soisores 7273 |
. . . . . . . . . . . . . . . . 17
β’ ((( <
Or (1...π) β§ π Or β) β§ (πΉ:(1...π)βΆβ β§ (π βͺ {π΅}) β (1...π))) β ((πΉ βΎ (π βͺ {π΅})) Isom < , π ((π βͺ {π΅}), (πΉ β (π βͺ {π΅}))) β βπ§ β (π βͺ {π΅})βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
138 | 66, 8, 137 | mpanl12 701 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:(1...π)βΆβ β§ (π βͺ {π΅}) β (1...π)) β ((πΉ βΎ (π βͺ {π΅})) Isom < , π ((π βͺ {π΅}), (πΉ β (π βͺ {π΅}))) β βπ§ β (π βͺ {π΅})βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
139 | 53, 136, 138 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((πΉ βΎ (π βͺ {π΅})) Isom < , π ((π βͺ {π΅}), (πΉ β (π βͺ {π΅}))) β βπ§ β (π βͺ {π΅})βπ€ β (π βͺ {π΅})(π§ < π€ β (πΉβπ§)π(πΉβπ€)))) |
140 | 134, 139 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΉ βΎ (π βͺ {π΅})) Isom < , π ((π βͺ {π΅}), (πΉ β (π βͺ {π΅})))) |
141 | | ssun2 4134 |
. . . . . . . . . . . . . . 15
β’ {π΅} β (π βͺ {π΅}) |
142 | | snssg 4745 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β (1...π΅) β (π΅ β (π βͺ {π΅}) β {π΅} β (π βͺ {π΅}))) |
143 | 47, 142 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (π΅ β (π βͺ {π΅}) β {π΅} β (π βͺ {π΅}))) |
144 | 141, 143 | mpbiri 258 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β π΅ β (π βͺ {π΅})) |
145 | 22 | erdszelem1 33842 |
. . . . . . . . . . . . . 14
β’ ((π βͺ {π΅}) β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)} β ((π βͺ {π΅}) β (1...π΅) β§ (πΉ βΎ (π βͺ {π΅})) Isom < , π ((π βͺ {π΅}), (πΉ β (π βͺ {π΅}))) β§ π΅ β (π βͺ {π΅}))) |
146 | 49, 140, 144, 145 | syl3anbrc 1344 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (π βͺ {π΅}) β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) |
147 | | vex 3448 |
. . . . . . . . . . . . . . . 16
β’ π β V |
148 | | snex 5389 |
. . . . . . . . . . . . . . . 16
β’ {π΅} β V |
149 | 147, 148 | unex 7681 |
. . . . . . . . . . . . . . 15
β’ (π βͺ {π΅}) β V |
150 | 1 | fdmi 6681 |
. . . . . . . . . . . . . . 15
β’ dom
β― = V |
151 | 149, 150 | eleqtrri 2833 |
. . . . . . . . . . . . . 14
β’ (π βͺ {π΅}) β dom β― |
152 | | funfvima 7181 |
. . . . . . . . . . . . . 14
β’ ((Fun
β― β§ (π βͺ
{π΅}) β dom β―)
β ((π βͺ {π΅}) β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)} β (β―β(π βͺ {π΅})) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}))) |
153 | 3, 151, 152 | mp2an 691 |
. . . . . . . . . . . . 13
β’ ((π βͺ {π΅}) β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)} β (β―β(π βͺ {π΅})) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})) |
154 | 146, 153 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β―β(π βͺ {π΅})) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})) |
155 | 154 | ne0d 4296 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β
) |
156 | 23 | simpli 485 |
. . . . . . . . . . . 12
β’ (β―
β {π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β Fin |
157 | | fimaxre2 12105 |
. . . . . . . . . . . 12
β’
(((β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β β§ (β― β
{π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β Fin) β βπ§ β β βπ€ β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})π€ β€ π§) |
158 | 27, 156, 157 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β βπ§ β β βπ€ β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})π€ β€ π§) |
159 | 33, 36 | ltnled 11307 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ < π΅ β Β¬ π΅ β€ π΄)) |
160 | 37, 159 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (π β Β¬ π΅ β€ π΄) |
161 | | elfzle2 13451 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β (1...π΄) β π΅ β€ π΄) |
162 | 160, 161 | nsyl 140 |
. . . . . . . . . . . . . . 15
β’ (π β Β¬ π΅ β (1...π΄)) |
163 | 162 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β Β¬ π΅ β (1...π΄)) |
164 | 16, 163 | ssneldd 3948 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β Β¬ π΅ β π) |
165 | | hashunsng 14298 |
. . . . . . . . . . . . . 14
β’ (π΅ β (1...π) β ((π β Fin β§ Β¬ π΅ β π) β (β―β(π βͺ {π΅})) = ((β―βπ) + 1))) |
166 | 98, 165 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((π β Fin β§ Β¬ π΅ β π) β (β―β(π βͺ {π΅})) = ((β―βπ) + 1))) |
167 | 18, 164, 166 | mp2and 698 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β―β(π βͺ {π΅})) = ((β―βπ) + 1)) |
168 | 167, 154 | eqeltrrd 2835 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((β―βπ) + 1) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})) |
169 | | suprub 12121 |
. . . . . . . . . . 11
β’
((((β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β β§ (β― β
{π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}) β β
β§ βπ§ β β βπ€ β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})π€ β€ π§) β§ ((β―βπ) + 1) β (β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)})) β ((β―βπ) + 1) β€ sup((β― β
{π¦ β π«
(1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}), β, < )) |
170 | 27, 155, 158, 168, 169 | syl31anc 1374 |
. . . . . . . . . 10
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((β―βπ) + 1) β€ sup((β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}), β, < )) |
171 | 5, 6, 7 | erdszelem3 33844 |
. . . . . . . . . . . 12
β’ (π΅ β (1...π) β (πΎβπ΅) = sup((β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}), β, < )) |
172 | 29, 171 | syl 17 |
. . . . . . . . . . 11
β’ (π β (πΎβπ΅) = sup((β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}), β, < )) |
173 | 172 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΎβπ΅) = sup((β― β {π¦ β π« (1...π΅) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΅ β π¦)}), β, < )) |
174 | 170, 173 | breqtrrd 5134 |
. . . . . . . . 9
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((β―βπ) + 1) β€ (πΎβπ΅)) |
175 | 5, 6, 7, 8 | erdszelem6 33847 |
. . . . . . . . . . . . 13
β’ (π β πΎ:(1...π)βΆβ) |
176 | 175, 29 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ (π β (πΎβπ΅) β β) |
177 | 176 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΎβπ΅) β β) |
178 | 177 | nnnn0d 12478 |
. . . . . . . . . 10
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (πΎβπ΅) β
β0) |
179 | | nn0ltp1le 12566 |
. . . . . . . . . 10
β’
(((β―βπ)
β β0 β§ (πΎβπ΅) β β0) β
((β―βπ) <
(πΎβπ΅) β ((β―βπ) + 1) β€ (πΎβπ΅))) |
180 | 20, 178, 179 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β ((β―βπ) < (πΎβπ΅) β ((β―βπ) + 1) β€ (πΎβπ΅))) |
181 | 174, 180 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β―βπ) < (πΎβπ΅)) |
182 | 21, 181 | ltned 11296 |
. . . . . . 7
β’ (((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β§ (πΉβπ΄)π(πΉβπ΅)) β (β―βπ) β (πΎβπ΅)) |
183 | 182 | ex 414 |
. . . . . 6
β’ ((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β ((πΉβπ΄)π(πΉβπ΅) β (β―βπ) β (πΎβπ΅))) |
184 | | neeq1 3003 |
. . . . . . 7
β’
((β―βπ) =
(πΎβπ΄) β ((β―βπ) β (πΎβπ΅) β (πΎβπ΄) β (πΎβπ΅))) |
185 | 184 | imbi2d 341 |
. . . . . 6
β’
((β―βπ) =
(πΎβπ΄) β (((πΉβπ΄)π(πΉβπ΅) β (β―βπ) β (πΎβπ΅)) β ((πΉβπ΄)π(πΉβπ΅) β (πΎβπ΄) β (πΎβπ΅)))) |
186 | 183, 185 | syl5ibcom 244 |
. . . . 5
β’ ((π β§ (π β (1...π΄) β§ (πΉ βΎ π) Isom < , π (π, (πΉ β π)) β§ π΄ β π)) β ((β―βπ) = (πΎβπ΄) β ((πΉβπ΄)π(πΉβπ΅) β (πΎβπ΄) β (πΎβπ΅)))) |
187 | 14, 186 | sylan2b 595 |
. . . 4
β’ ((π β§ π β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)}) β ((β―βπ) = (πΎβπ΄) β ((πΉβπ΄)π(πΉβπ΅) β (πΎβπ΄) β (πΎβπ΅)))) |
188 | 187 | rexlimdva 3149 |
. . 3
β’ (π β (βπ β {π¦ β π« (1...π΄) β£ ((πΉ βΎ π¦) Isom < , π (π¦, (πΉ β π¦)) β§ π΄ β π¦)} (β―βπ) = (πΎβπ΄) β ((πΉβπ΄)π(πΉβπ΅) β (πΎβπ΄) β (πΎβπ΅)))) |
189 | 12, 188 | mpd 15 |
. 2
β’ (π β ((πΉβπ΄)π(πΉβπ΅) β (πΎβπ΄) β (πΎβπ΅))) |
190 | 189 | necon2bd 2956 |
1
β’ (π β ((πΎβπ΄) = (πΎβπ΅) β Β¬ (πΉβπ΄)π(πΉβπ΅))) |