Step | Hyp | Ref
| Expression |
1 | | 3simpb 1149 |
. . 3
โข ((๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โ (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ)) |
2 | 1 | reximi 3087 |
. 2
โข
(โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โ โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ)) |
3 | | fveq2 6842 |
. . . . . 6
โข (๐ = ๐ค โ (โคโฅโ๐) =
(โคโฅโ๐ค)) |
4 | 3 | sseq2d 3976 |
. . . . 5
โข (๐ = ๐ค โ (๐ด โ (โคโฅโ๐) โ ๐ด โ (โคโฅโ๐ค))) |
5 | | seqeq1 13909 |
. . . . . 6
โข (๐ = ๐ค โ seq๐( ยท , ๐น) = seq๐ค( ยท , ๐น)) |
6 | 5 | breq1d 5115 |
. . . . 5
โข (๐ = ๐ค โ (seq๐( ยท , ๐น) โ ๐ฅ โ seq๐ค( ยท , ๐น) โ ๐ฅ)) |
7 | 4, 6 | anbi12d 631 |
. . . 4
โข (๐ = ๐ค โ ((๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โ (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ))) |
8 | 7 | cbvrexvw 3226 |
. . 3
โข
(โ๐ โ
โค (๐ด โ
(โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ) โ โ๐ค โ โค (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ)) |
9 | | reeanv 3217 |
. . . . 5
โข
(โ๐ค โ
โค โ๐ โ
โ ((๐ด โ
(โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ (โ๐ค โ โค (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)))) |
10 | | simprlr 778 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ seq๐ค( ยท , ๐น) โ ๐ฅ) |
11 | | simprll 777 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ ๐ด โ (โคโฅโ๐ค)) |
12 | | uzssz 12784 |
. . . . . . . . . . . . . . . . 17
โข
(โคโฅโ๐ค) โ โค |
13 | | zssre 12506 |
. . . . . . . . . . . . . . . . 17
โข โค
โ โ |
14 | 12, 13 | sstri 3953 |
. . . . . . . . . . . . . . . 16
โข
(โคโฅโ๐ค) โ โ |
15 | 11, 14 | sstrdi 3956 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ ๐ด โ โ) |
16 | | ltso 11235 |
. . . . . . . . . . . . . . 15
โข < Or
โ |
17 | | soss 5565 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ โ ( <
Or โ โ < Or ๐ด)) |
18 | 15, 16, 17 | mpisyl 21 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ < Or ๐ด) |
19 | | fzfi 13877 |
. . . . . . . . . . . . . . 15
โข
(1...๐) โ
Fin |
20 | | ovex 7390 |
. . . . . . . . . . . . . . . . . 18
โข
(1...๐) โ
V |
21 | 20 | f1oen 8913 |
. . . . . . . . . . . . . . . . 17
โข (๐:(1...๐)โ1-1-ontoโ๐ด โ (1...๐) โ ๐ด) |
22 | 21 | ad2antll 727 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ (1...๐) โ ๐ด) |
23 | 22 | ensymd 8945 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ ๐ด โ (1...๐)) |
24 | | enfii 9133 |
. . . . . . . . . . . . . . 15
โข
(((1...๐) โ Fin
โง ๐ด โ (1...๐)) โ ๐ด โ Fin) |
25 | 19, 23, 24 | sylancr 587 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ ๐ด โ Fin) |
26 | | fz1iso 14361 |
. . . . . . . . . . . . . 14
โข (( <
Or ๐ด โง ๐ด โ Fin) โ โ๐ ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด)) |
27 | 18, 25, 26 | syl2anc 584 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ โ๐ ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด)) |
28 | | prodmo.1 |
. . . . . . . . . . . . . . . 16
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) |
29 | | prodmo.2 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
30 | 29 | ad4ant14 750 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โง ๐ โ ๐ด) โ ๐ต โ โ) |
31 | | prodmo.3 |
. . . . . . . . . . . . . . . 16
โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
32 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โฆ
โฆ(๐โ๐) / ๐โฆ๐ต) = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) |
33 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โ ๐ โ โ) |
34 | | simplrl 775 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โ ๐ค โ โค) |
35 | | simplll 773 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ
(โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด)) โ ๐ด โ (โคโฅโ๐ค)) |
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โ ๐ด โ (โคโฅโ๐ค)) |
37 | | simprlr 778 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โ ๐:(1...๐)โ1-1-ontoโ๐ด) |
38 | | simprr 771 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โ ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด)) |
39 | 28, 30, 31, 32, 33, 34, 36, 37, 38 | prodmolem2a 15817 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด) โง ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด))) โ seq๐ค( ยท , ๐น) โ (seq1( ยท , ๐บ)โ๐)) |
40 | 39 | expr 457 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ (๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด) โ seq๐ค( ยท , ๐น) โ (seq1( ยท , ๐บ)โ๐))) |
41 | 40 | exlimdv 1936 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ (โ๐ ๐ Isom < , < ((1...(โฏโ๐ด)), ๐ด) โ seq๐ค( ยท , ๐น) โ (seq1( ยท , ๐บ)โ๐))) |
42 | 27, 41 | mpd 15 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ seq๐ค( ยท , ๐น) โ (seq1( ยท , ๐บ)โ๐)) |
43 | | climuni 15434 |
. . . . . . . . . . . 12
โข
((seq๐ค( ยท ,
๐น) โ ๐ฅ โง seq๐ค( ยท , ๐น) โ (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐)) |
44 | 10, 42, 43 | syl2anc 584 |
. . . . . . . . . . 11
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ ๐ฅ = (seq1( ยท , ๐บ)โ๐)) |
45 | | eqeq2 2748 |
. . . . . . . . . . 11
โข (๐ง = (seq1( ยท , ๐บ)โ๐) โ (๐ฅ = ๐ง โ ๐ฅ = (seq1( ยท , ๐บ)โ๐))) |
46 | 44, 45 | syl5ibrcom 246 |
. . . . . . . . . 10
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง ๐:(1...๐)โ1-1-ontoโ๐ด)) โ (๐ง = (seq1( ยท , ๐บ)โ๐) โ ๐ฅ = ๐ง)) |
47 | 46 | expr 457 |
. . . . . . . . 9
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ)) โ (๐:(1...๐)โ1-1-ontoโ๐ด โ (๐ง = (seq1( ยท , ๐บ)โ๐) โ ๐ฅ = ๐ง))) |
48 | 47 | impd 411 |
. . . . . . . 8
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ)) โ ((๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |
49 | 48 | exlimdv 1936 |
. . . . . . 7
โข (((๐ โง (๐ค โ โค โง ๐ โ โ)) โง (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ)) โ (โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |
50 | 49 | expimpd 454 |
. . . . . 6
โข ((๐ โง (๐ค โ โค โง ๐ โ โ)) โ (((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ ๐ฅ = ๐ง)) |
51 | 50 | rexlimdvva 3205 |
. . . . 5
โข (๐ โ (โ๐ค โ โค โ๐ โ โ ((๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ ๐ฅ = ๐ง)) |
52 | 9, 51 | biimtrrid 242 |
. . . 4
โข (๐ โ ((โ๐ค โ โค (๐ด โ
(โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ) โง โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐))) โ ๐ฅ = ๐ง)) |
53 | 52 | expdimp 453 |
. . 3
โข ((๐ โง โ๐ค โ โค (๐ด โ (โคโฅโ๐ค) โง seq๐ค( ยท , ๐น) โ ๐ฅ)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |
54 | 8, 53 | sylan2b 594 |
. 2
โข ((๐ โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง seq๐( ยท , ๐น) โ ๐ฅ)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |
55 | 2, 54 | sylan2 593 |
1
โข ((๐ โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ
(โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) |