Step | Hyp | Ref
| Expression |
1 | | 2lgslem1b.f |
. . . 4
โข ๐น = (๐ โ ๐ผ โฆ (๐ ยท 2)) |
2 | | eqeq1 2741 |
. . . . . 6
โข (๐ฅ = (๐ ยท 2) โ (๐ฅ = (๐ ยท 2) โ (๐ ยท 2) = (๐ ยท 2))) |
3 | 2 | rexbidv 3176 |
. . . . 5
โข (๐ฅ = (๐ ยท 2) โ (โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2) โ โ๐ โ ๐ผ (๐ ยท 2) = (๐ ยท 2))) |
4 | | elfzelz 13442 |
. . . . . . 7
โข (๐ โ (๐ด...๐ต) โ ๐ โ โค) |
5 | | 2lgslem1b.i |
. . . . . . 7
โข ๐ผ = (๐ด...๐ต) |
6 | 4, 5 | eleq2s 2856 |
. . . . . 6
โข (๐ โ ๐ผ โ ๐ โ โค) |
7 | | 2z 12536 |
. . . . . . 7
โข 2 โ
โค |
8 | 7 | a1i 11 |
. . . . . 6
โข (๐ โ ๐ผ โ 2 โ โค) |
9 | 6, 8 | zmulcld 12614 |
. . . . 5
โข (๐ โ ๐ผ โ (๐ ยท 2) โ โค) |
10 | | id 22 |
. . . . . 6
โข (๐ โ ๐ผ โ ๐ โ ๐ผ) |
11 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท 2) = (๐ ยท 2)) |
12 | 11 | eqeq2d 2748 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท 2) = (๐ ยท 2) โ (๐ ยท 2) = (๐ ยท 2))) |
13 | 12 | adantl 483 |
. . . . . 6
โข ((๐ โ ๐ผ โง ๐ = ๐) โ ((๐ ยท 2) = (๐ ยท 2) โ (๐ ยท 2) = (๐ ยท 2))) |
14 | | eqidd 2738 |
. . . . . 6
โข (๐ โ ๐ผ โ (๐ ยท 2) = (๐ ยท 2)) |
15 | 10, 13, 14 | rspcedvd 3584 |
. . . . 5
โข (๐ โ ๐ผ โ โ๐ โ ๐ผ (๐ ยท 2) = (๐ ยท 2)) |
16 | 3, 9, 15 | elrabd 3648 |
. . . 4
โข (๐ โ ๐ผ โ (๐ ยท 2) โ {๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)}) |
17 | 1, 16 | fmpti 7061 |
. . 3
โข ๐น:๐ผโถ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} |
18 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ฆ โ (๐ ยท 2) = (๐ฆ ยท 2)) |
19 | | simpl 484 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ๐ฆ โ ๐ผ) |
20 | | ovexd 7393 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ (๐ฆ ยท 2) โ V) |
21 | 1, 18, 19, 20 | fvmptd3 6972 |
. . . . . 6
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ (๐นโ๐ฆ) = (๐ฆ ยท 2)) |
22 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ง โ (๐ ยท 2) = (๐ง ยท 2)) |
23 | | simpr 486 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ๐ง โ ๐ผ) |
24 | | ovexd 7393 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ (๐ง ยท 2) โ V) |
25 | 1, 22, 23, 24 | fvmptd3 6972 |
. . . . . 6
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ (๐นโ๐ง) = (๐ง ยท 2)) |
26 | 21, 25 | eqeq12d 2753 |
. . . . 5
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ (๐ฆ ยท 2) = (๐ง ยท 2))) |
27 | | elfzelz 13442 |
. . . . . . . . . 10
โข (๐ฆ โ (๐ด...๐ต) โ ๐ฆ โ โค) |
28 | 27, 5 | eleq2s 2856 |
. . . . . . . . 9
โข (๐ฆ โ ๐ผ โ ๐ฆ โ โค) |
29 | 28 | zcnd 12609 |
. . . . . . . 8
โข (๐ฆ โ ๐ผ โ ๐ฆ โ โ) |
30 | 29 | adantr 482 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ๐ฆ โ โ) |
31 | | elfzelz 13442 |
. . . . . . . . . 10
โข (๐ง โ (๐ด...๐ต) โ ๐ง โ โค) |
32 | 31, 5 | eleq2s 2856 |
. . . . . . . . 9
โข (๐ง โ ๐ผ โ ๐ง โ โค) |
33 | 32 | zcnd 12609 |
. . . . . . . 8
โข (๐ง โ ๐ผ โ ๐ง โ โ) |
34 | 33 | adantl 483 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ๐ง โ โ) |
35 | | 2cnd 12232 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ 2 โ โ) |
36 | | 2ne0 12258 |
. . . . . . . 8
โข 2 โ
0 |
37 | 36 | a1i 11 |
. . . . . . 7
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ 2 โ 0) |
38 | 30, 34, 35, 37 | mulcan2d 11790 |
. . . . . 6
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ((๐ฆ ยท 2) = (๐ง ยท 2) โ ๐ฆ = ๐ง)) |
39 | 38 | biimpd 228 |
. . . . 5
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ((๐ฆ ยท 2) = (๐ง ยท 2) โ ๐ฆ = ๐ง)) |
40 | 26, 39 | sylbid 239 |
. . . 4
โข ((๐ฆ โ ๐ผ โง ๐ง โ ๐ผ) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
41 | 40 | rgen2 3195 |
. . 3
โข
โ๐ฆ โ
๐ผ โ๐ง โ ๐ผ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง) |
42 | | dff13 7203 |
. . 3
โข (๐น:๐ผโ1-1โ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} โ (๐น:๐ผโถ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} โง โ๐ฆ โ ๐ผ โ๐ง โ ๐ผ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง))) |
43 | 17, 41, 42 | mpbir2an 710 |
. 2
โข ๐น:๐ผโ1-1โ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} |
44 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท 2) = (๐ ยท 2)) |
45 | 44 | eqeq2d 2748 |
. . . . . 6
โข (๐ = ๐ โ (๐ฅ = (๐ ยท 2) โ ๐ฅ = (๐ ยท 2))) |
46 | 45 | cbvrexvw 3227 |
. . . . 5
โข
(โ๐ โ
๐ผ ๐ฅ = (๐ ยท 2) โ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)) |
47 | | elfzelz 13442 |
. . . . . . . . . 10
โข (๐ โ (๐ด...๐ต) โ ๐ โ โค) |
48 | 7 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ (๐ด...๐ต) โ 2 โ โค) |
49 | 47, 48 | zmulcld 12614 |
. . . . . . . . 9
โข (๐ โ (๐ด...๐ต) โ (๐ ยท 2) โ โค) |
50 | 49, 5 | eleq2s 2856 |
. . . . . . . 8
โข (๐ โ ๐ผ โ (๐ ยท 2) โ โค) |
51 | | eleq1 2826 |
. . . . . . . 8
โข (๐ฅ = (๐ ยท 2) โ (๐ฅ โ โค โ (๐ ยท 2) โ
โค)) |
52 | 50, 51 | syl5ibrcom 247 |
. . . . . . 7
โข (๐ โ ๐ผ โ (๐ฅ = (๐ ยท 2) โ ๐ฅ โ โค)) |
53 | 52 | rexlimiv 3146 |
. . . . . 6
โข
(โ๐ โ
๐ผ ๐ฅ = (๐ ยท 2) โ ๐ฅ โ โค) |
54 | 53 | pm4.71ri 562 |
. . . . 5
โข
(โ๐ โ
๐ผ ๐ฅ = (๐ ยท 2) โ (๐ฅ โ โค โง โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2))) |
55 | 46, 54 | bitri 275 |
. . . 4
โข
(โ๐ โ
๐ผ ๐ฅ = (๐ ยท 2) โ (๐ฅ โ โค โง โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2))) |
56 | 55 | abbii 2807 |
. . 3
โข {๐ฅ โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} = {๐ฅ โฃ (๐ฅ โ โค โง โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2))} |
57 | 1 | rnmpt 5911 |
. . 3
โข ran ๐น = {๐ฅ โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} |
58 | | df-rab 3409 |
. . 3
โข {๐ฅ โ โค โฃ
โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} = {๐ฅ โฃ (๐ฅ โ โค โง โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2))} |
59 | 56, 57, 58 | 3eqtr4i 2775 |
. 2
โข ran ๐น = {๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} |
60 | | dff1o5 6794 |
. 2
โข (๐น:๐ผโ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} โ (๐น:๐ผโ1-1โ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} โง ran ๐น = {๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)})) |
61 | 43, 59, 60 | mpbir2an 710 |
1
โข ๐น:๐ผโ1-1-ontoโ{๐ฅ โ โค โฃ โ๐ โ ๐ผ ๐ฅ = (๐ ยท 2)} |