Step | Hyp | Ref
| Expression |
1 | | tocyccntz.s |
. 2
β’ π = (SymGrpβπ·) |
2 | | eqid 2733 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
3 | | tocyccntz.z |
. 2
β’ π = (Cntzβπ) |
4 | | tocyccntz.1 |
. . 3
β’ (π β π· β π) |
5 | | tocyccntz.m |
. . . 4
β’ π = (toCycβπ·) |
6 | 5, 1, 2 | tocycf 32015 |
. . 3
β’ (π· β π β π:{π β Word π· β£ π:dom πβ1-1βπ·}βΆ(Baseβπ)) |
7 | | fimass 6690 |
. . 3
β’ (π:{π β Word π· β£ π:dom πβ1-1βπ·}βΆ(Baseβπ) β (π β π΄) β (Baseβπ)) |
8 | 4, 6, 7 | 3syl 18 |
. 2
β’ (π β (π β π΄) β (Baseβπ)) |
9 | | difss 4092 |
. . . . . . 7
β’ (π΄ β (β‘β― β {0, 1})) β π΄ |
10 | | tocyccntz.2 |
. . . . . . 7
β’ (π β Disj π₯ β π΄ ran π₯) |
11 | | disjss1 5077 |
. . . . . . 7
β’ ((π΄ β (β‘β― β {0, 1})) β π΄ β (Disj π₯ β π΄ ran π₯ β Disj π₯ β (π΄ β (β‘β― β {0, 1}))ran π₯)) |
12 | 9, 10, 11 | mpsyl 68 |
. . . . . 6
β’ (π β Disj π₯ β (π΄ β (β‘β― β {0, 1}))ran π₯) |
13 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π· β π) |
14 | | tocyccntz.a |
. . . . . . . . . . . . . 14
β’ (π β π΄ β dom π) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π΄ β dom π) |
16 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π₯ β (π΄ β (β‘β― β {0, 1}))) |
17 | 16 | eldifad 3923 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π₯ β π΄) |
18 | 15, 17 | sseldd 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π₯ β dom π) |
19 | | fdm 6678 |
. . . . . . . . . . . . 13
β’ (π:{π β Word π· β£ π:dom πβ1-1βπ·}βΆ(Baseβπ) β dom π = {π β Word π· β£ π:dom πβ1-1βπ·}) |
20 | 13, 6, 19 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β dom π = {π β Word π· β£ π:dom πβ1-1βπ·}) |
21 | 18, 20 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π₯ β {π β Word π· β£ π:dom πβ1-1βπ·}) |
22 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = π₯ β π = π₯) |
23 | | dmeq 5860 |
. . . . . . . . . . . . 13
β’ (π = π₯ β dom π = dom π₯) |
24 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ (π = π₯ β π· = π·) |
25 | 22, 23, 24 | f1eq123d 6777 |
. . . . . . . . . . . 12
β’ (π = π₯ β (π:dom πβ1-1βπ· β π₯:dom π₯β1-1βπ·)) |
26 | 25 | elrab 3646 |
. . . . . . . . . . 11
β’ (π₯ β {π β Word π· β£ π:dom πβ1-1βπ·} β (π₯ β Word π· β§ π₯:dom π₯β1-1βπ·)) |
27 | 21, 26 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β (π₯ β Word π· β§ π₯:dom π₯β1-1βπ·)) |
28 | 27 | simpld 496 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π₯ β Word π·) |
29 | 27 | simprd 497 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β π₯:dom π₯β1-1βπ·) |
30 | 16 | eldifbd 3924 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β Β¬ π₯ β (β‘β― β {0, 1})) |
31 | | hashgt1 31759 |
. . . . . . . . . . 11
β’ (π₯ β V β (Β¬ π₯ β (β‘β― β {0, 1}) β 1 <
(β―βπ₯))) |
32 | 31 | elv 3450 |
. . . . . . . . . 10
β’ (Β¬
π₯ β (β‘β― β {0, 1}) β 1 <
(β―βπ₯)) |
33 | 30, 32 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β 1 <
(β―βπ₯)) |
34 | 5, 13, 28, 29, 33 | cycpmrn 32041 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β ran π₯ = dom ((πβπ₯) β I )) |
35 | 16 | fvresd 6863 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) = (πβπ₯)) |
36 | 35 | difeq1d 4082 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I ) = ((πβπ₯) β I )) |
37 | 36 | dmeqd 5862 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β dom
(((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I ) = dom ((πβπ₯) β I )) |
38 | 34, 37 | eqtr4d 2776 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β ran π₯ = dom (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I )) |
39 | 38 | disjeq2dv 5076 |
. . . . . 6
β’ (π β (Disj π₯ β (π΄ β (β‘β― β {0, 1}))ran π₯ β Disj π₯ β (π΄ β (β‘β― β {0, 1}))dom (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I ))) |
40 | 12, 39 | mpbid 231 |
. . . . 5
β’ (π β Disj π₯ β (π΄ β (β‘β― β {0, 1}))dom (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I )) |
41 | 4, 6 | syl 17 |
. . . . . . . . . . 11
β’ (π β π:{π β Word π· β£ π:dom πβ1-1βπ·}βΆ(Baseβπ)) |
42 | 41 | ffdmd 6700 |
. . . . . . . . . 10
β’ (π β π:dom πβΆ(Baseβπ)) |
43 | 14 | ssdifssd 4103 |
. . . . . . . . . 10
β’ (π β (π΄ β (β‘β― β {0, 1})) β dom π) |
44 | 42, 43 | fssresd 6710 |
. . . . . . . . 9
β’ (π β (π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0,
1}))βΆ(Baseβπ)) |
45 | 41, 14 | fssdmd 6688 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β {π β Word π· β£ π:dom πβ1-1βπ·}) |
46 | 45 | ad4antr 731 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π΄ β {π β Word π· β£ π:dom πβ1-1βπ·}) |
47 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π β (π΄ β (β‘β― β {0, 1}))) |
48 | 47 | eldifad 3923 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π β π΄) |
49 | 46, 48 | sseldd 3946 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π β {π β Word π· β£ π:dom πβ1-1βπ·}) |
50 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β π = π ) |
51 | | dmeq 5860 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β dom π = dom π ) |
52 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β π· = π·) |
53 | 50, 51, 52 | f1eq123d 6777 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π:dom πβ1-1βπ· β π :dom π β1-1βπ·)) |
54 | 53 | elrab 3646 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π β Word π· β£ π:dom πβ1-1βπ·} β (π β Word π· β§ π :dom π β1-1βπ·)) |
55 | 49, 54 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β (π β Word π· β§ π :dom π β1-1βπ·)) |
56 | 55 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π β Word π·) |
57 | | wrdf 14413 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π· β π :(0..^(β―βπ ))βΆπ·) |
58 | | frel 6674 |
. . . . . . . . . . . . . . . 16
β’ (π :(0..^(β―βπ ))βΆπ· β Rel π ) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β Rel π ) |
60 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) |
61 | 47 | fvresd 6863 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = (πβπ )) |
62 | 16 | ad5ant13 756 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯ β (π΄ β (β‘β― β {0, 1}))) |
63 | 62 | fvresd 6863 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) = (πβπ₯)) |
64 | 60, 61, 63 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β (πβπ₯) = (πβπ )) |
65 | 64 | difeq1d 4082 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ((πβπ₯) β I ) = ((πβπ ) β I )) |
66 | 65 | dmeqd 5862 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β dom ((πβπ₯) β I ) = dom ((πβπ ) β I )) |
67 | 4 | ad4antr 731 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π· β π) |
68 | 17 | ad5ant13 756 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯ β π΄) |
69 | 46, 68 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯ β {π β Word π· β£ π:dom πβ1-1βπ·}) |
70 | 69, 26 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β (π₯ β Word π· β§ π₯:dom π₯β1-1βπ·)) |
71 | 70 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯ β Word π·) |
72 | 70 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯:dom π₯β1-1βπ·) |
73 | 33 | ad5ant13 756 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β 1 < (β―βπ₯)) |
74 | 5, 67, 71, 72, 73 | cycpmrn 32041 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ran π₯ = dom ((πβπ₯) β I )) |
75 | 55 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π :dom π β1-1βπ·) |
76 | 14 | ssdifd 4101 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΄ β (β‘β― β {0, 1})) β (dom π β (β‘β― β {0, 1}))) |
77 | 76 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π΄ β (β‘β― β {0, 1}))) β π β (dom π β (β‘β― β {0, 1}))) |
78 | 77 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π β (dom π β (β‘β― β {0, 1}))) |
79 | 78 | eldifbd 3924 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β Β¬ π β (β‘β― β {0, 1})) |
80 | | hashgt1 31759 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β (Β¬ π β (β‘β― β {0, 1}) β 1 <
(β―βπ ))) |
81 | 80 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π΄ β§ Β¬ π β (β‘β― β {0, 1})) β 1 <
(β―βπ )) |
82 | 48, 79, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β 1 < (β―βπ )) |
83 | 5, 67, 56, 75, 82 | cycpmrn 32041 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ran π = dom ((πβπ ) β I )) |
84 | 66, 74, 83 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ran π = ran π₯) |
85 | 84 | ineq2d 4173 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β (ran π₯ β© ran π ) = (ran π₯ β© ran π₯)) |
86 | | inidm 4179 |
. . . . . . . . . . . . . . . . . 18
β’ (ran
π₯ β© ran π₯) = ran π₯ |
87 | 85, 86 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β (ran π₯ β© ran π ) = ran π₯) |
88 | | rneq 5892 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β ran π₯ = ran π¦) |
89 | 88 | cbvdisjv 5082 |
. . . . . . . . . . . . . . . . . . . 20
β’
(Disj π₯
β π΄ ran π₯ β Disj π¦ β π΄ ran π¦) |
90 | 10, 89 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Disj π¦ β π΄ ran π¦) |
91 | 90 | ad4antr 731 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β Disj π¦ β π΄ ran π¦) |
92 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β Β¬ π = π₯) |
93 | 92 | neqned 2947 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π β π₯) |
94 | 93 | necomd 2996 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯ β π ) |
95 | | rneq 5892 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π₯ β ran π¦ = ran π₯) |
96 | | rneq 5892 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β ran π¦ = ran π ) |
97 | 95, 96 | disji2 5088 |
. . . . . . . . . . . . . . . . . 18
β’
((Disj π¦
β π΄ ran π¦ β§ (π₯ β π΄ β§ π β π΄) β§ π₯ β π ) β (ran π₯ β© ran π ) = β
) |
98 | 91, 68, 48, 94, 97 | syl121anc 1376 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β (ran π₯ β© ran π ) = β
) |
99 | 87, 98 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ran π₯ = β
) |
100 | 84, 99 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β ran π = β
) |
101 | | relrn0 5925 |
. . . . . . . . . . . . . . . 16
β’ (Rel
π β (π = β
β ran π = β
)) |
102 | 101 | biimpar 479 |
. . . . . . . . . . . . . . 15
β’ ((Rel
π β§ ran π = β
) β π = β
) |
103 | 59, 100, 102 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π = β
) |
104 | | wrdf 14413 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β Word π· β π₯:(0..^(β―βπ₯))βΆπ·) |
105 | | frel 6674 |
. . . . . . . . . . . . . . . 16
β’ (π₯:(0..^(β―βπ₯))βΆπ· β Rel π₯) |
106 | 71, 104, 105 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β Rel π₯) |
107 | | relrn0 5925 |
. . . . . . . . . . . . . . . 16
β’ (Rel
π₯ β (π₯ = β
β ran π₯ = β
)) |
108 | 107 | biimpar 479 |
. . . . . . . . . . . . . . 15
β’ ((Rel
π₯ β§ ran π₯ = β
) β π₯ = β
) |
109 | 106, 99, 108 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π₯ = β
) |
110 | 103, 109 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β§ Β¬ π = π₯) β π = π₯) |
111 | 110 | pm2.18da 799 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β§ ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β π = π₯) |
112 | 111 | ex 414 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ β (β‘β― β {0, 1}))) β§ π₯ β (π΄ β (β‘β― β {0, 1}))) β (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β π = π₯)) |
113 | 112 | anasss 468 |
. . . . . . . . . 10
β’ ((π β§ (π β (π΄ β (β‘β― β {0, 1})) β§ π₯ β (π΄ β (β‘β― β {0, 1})))) β (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β π = π₯)) |
114 | 113 | ralrimivva 3194 |
. . . . . . . . 9
β’ (π β βπ β (π΄ β (β‘β― β {0, 1}))βπ₯ β (π΄ β (β‘β― β {0, 1}))(((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β π = π₯)) |
115 | | dff13 7203 |
. . . . . . . . 9
β’ ((π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1β(Baseβπ) β ((π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0,
1}))βΆ(Baseβπ)
β§ βπ β
(π΄ β (β‘β― β {0, 1}))βπ₯ β (π΄ β (β‘β― β {0, 1}))(((π βΎ (π΄ β (β‘β― β {0, 1})))βπ ) = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β π = π₯))) |
116 | 44, 114, 115 | sylanbrc 584 |
. . . . . . . 8
β’ (π β (π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1β(Baseβπ)) |
117 | | f1f1orn 6796 |
. . . . . . . 8
β’ ((π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1β(Baseβπ) β (π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1-ontoβran
(π βΎ (π΄ β (β‘β― β {0, 1})))) |
118 | 116, 117 | syl 17 |
. . . . . . 7
β’ (π β (π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1-ontoβran
(π βΎ (π΄ β (β‘β― β {0, 1})))) |
119 | | df-ima 5647 |
. . . . . . . . 9
β’ (π β (π΄ β (β‘β― β {0, 1}))) = ran (π βΎ (π΄ β (β‘β― β {0, 1}))) |
120 | 119 | a1i 11 |
. . . . . . . 8
β’ (π β (π β (π΄ β (β‘β― β {0, 1}))) = ran (π βΎ (π΄ β (β‘β― β {0, 1})))) |
121 | 120 | f1oeq3d 6782 |
. . . . . . 7
β’ (π β ((π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1-ontoβ(π β (π΄ β (β‘β― β {0, 1}))) β (π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1-ontoβran
(π βΎ (π΄ β (β‘β― β {0, 1}))))) |
122 | 118, 121 | mpbird 257 |
. . . . . 6
β’ (π β (π βΎ (π΄ β (β‘β― β {0, 1}))):(π΄ β (β‘β― β {0, 1}))β1-1-ontoβ(π β (π΄ β (β‘β― β {0, 1})))) |
123 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β π = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) |
124 | 123 | difeq1d 4082 |
. . . . . . 7
β’ ((π β§ π = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β (π β I ) = (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I )) |
125 | 124 | dmeqd 5862 |
. . . . . 6
β’ ((π β§ π = ((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯)) β dom (π β I ) = dom (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I )) |
126 | 122, 125 | disjrdx 31555 |
. . . . 5
β’ (π β (Disj π₯ β (π΄ β (β‘β― β {0, 1}))dom (((π βΎ (π΄ β (β‘β― β {0, 1})))βπ₯) β I ) β Disj
π β (π β (π΄ β (β‘β― β {0, 1})))dom (π β I ))) |
127 | 40, 126 | mpbid 231 |
. . . 4
β’ (π β Disj π β (π β (π΄ β (β‘β― β {0, 1})))dom (π β I )) |
128 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β (πβπ₯) = π) |
129 | 4 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β π· β π) |
130 | 14 | ssrind 4196 |
. . . . . . . . . . . . 13
β’ (π β (π΄ β© (β‘β― β {0, 1})) β (dom π β© (β‘β― β {0, 1}))) |
131 | 130 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β (π΄ β© (β‘β― β {0, 1})) β (dom π β© (β‘β― β {0, 1}))) |
132 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β π₯ β (π΄ β© (β‘β― β {0, 1}))) |
133 | 131, 132 | sseldd 3946 |
. . . . . . . . . . 11
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β π₯ β (dom π β© (β‘β― β {0, 1}))) |
134 | 5 | tocyc01 32016 |
. . . . . . . . . . 11
β’ ((π· β π β§ π₯ β (dom π β© (β‘β― β {0, 1}))) β (πβπ₯) = ( I βΎ π·)) |
135 | 129, 133,
134 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β (πβπ₯) = ( I βΎ π·)) |
136 | 128, 135 | eqtr3d 2775 |
. . . . . . . . 9
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β π = ( I βΎ π·)) |
137 | 136 | difeq1d 4082 |
. . . . . . . 8
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β (π β I ) = (( I βΎ π·) β I )) |
138 | 137 | dmeqd 5862 |
. . . . . . 7
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β dom (π β I ) = dom (( I βΎ π·) β I )) |
139 | | resdifcom 5957 |
. . . . . . . . . 10
β’ (( I
βΎ π·) β I ) = ((
I β I ) βΎ π·) |
140 | | difid 4331 |
. . . . . . . . . . 11
β’ ( I
β I ) = β
|
141 | 140 | reseq1i 5934 |
. . . . . . . . . 10
β’ (( I
β I ) βΎ π·) =
(β
βΎ π·) |
142 | | 0res 31568 |
. . . . . . . . . 10
β’ (β
βΎ π·) =
β
|
143 | 139, 141,
142 | 3eqtri 2765 |
. . . . . . . . 9
β’ (( I
βΎ π·) β I ) =
β
|
144 | 143 | dmeqi 5861 |
. . . . . . . 8
β’ dom (( I
βΎ π·) β I ) =
dom β
|
145 | | dm0 5877 |
. . . . . . . 8
β’ dom
β
= β
|
146 | 144, 145 | eqtri 2761 |
. . . . . . 7
β’ dom (( I
βΎ π·) β I ) =
β
|
147 | 138, 146 | eqtrdi 2789 |
. . . . . 6
β’ ((((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β§ π₯ β (π΄ β© (β‘β― β {0, 1}))) β§ (πβπ₯) = π) β dom (π β I ) = β
) |
148 | 41 | ffund 6673 |
. . . . . . 7
β’ (π β Fun π) |
149 | | fvelima 6909 |
. . . . . . 7
β’ ((Fun
π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β
βπ₯ β (π΄ β© (β‘β― β {0, 1}))(πβπ₯) = π) |
150 | 148, 149 | sylan 581 |
. . . . . 6
β’ ((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β
βπ₯ β (π΄ β© (β‘β― β {0, 1}))(πβπ₯) = π) |
151 | 147, 150 | r19.29a 3156 |
. . . . 5
β’ ((π β§ π β (π β (π΄ β© (β‘β― β {0, 1})))) β dom (π β I ) =
β
) |
152 | 151 | disjxun0 31538 |
. . . 4
β’ (π β (Disj π β ((π β (π΄ β (β‘β― β {0, 1}))) βͺ (π β (π΄ β© (β‘β― β {0, 1}))))dom (π β I ) β Disj
π β (π β (π΄ β (β‘β― β {0, 1})))dom (π β I ))) |
153 | 127, 152 | mpbird 257 |
. . 3
β’ (π β Disj π β ((π β (π΄ β (β‘β― β {0, 1}))) βͺ (π β (π΄ β© (β‘β― β {0, 1}))))dom (π β I )) |
154 | | uncom 4114 |
. . . . . 6
β’ ((π β (π΄ β (β‘β― β {0, 1}))) βͺ (π β (π΄ β© (β‘β― β {0, 1})))) = ((π β (π΄ β© (β‘β― β {0, 1}))) βͺ (π β (π΄ β (β‘β― β {0, 1})))) |
155 | | imaundi 6103 |
. . . . . 6
β’ (π β ((π΄ β© (β‘β― β {0, 1})) βͺ (π΄ β (β‘β― β {0, 1})))) = ((π β (π΄ β© (β‘β― β {0, 1}))) βͺ (π β (π΄ β (β‘β― β {0, 1})))) |
156 | | inundif 4439 |
. . . . . . 7
β’ ((π΄ β© (β‘β― β {0, 1})) βͺ (π΄ β (β‘β― β {0, 1}))) = π΄ |
157 | 156 | imaeq2i 6012 |
. . . . . 6
β’ (π β ((π΄ β© (β‘β― β {0, 1})) βͺ (π΄ β (β‘β― β {0, 1})))) = (π β π΄) |
158 | 154, 155,
157 | 3eqtr2i 2767 |
. . . . 5
β’ ((π β (π΄ β (β‘β― β {0, 1}))) βͺ (π β (π΄ β© (β‘β― β {0, 1})))) = (π β π΄) |
159 | 158 | a1i 11 |
. . . 4
β’ (π β ((π β (π΄ β (β‘β― β {0, 1}))) βͺ (π β (π΄ β© (β‘β― β {0, 1})))) = (π β π΄)) |
160 | 159 | disjeq1d 5079 |
. . 3
β’ (π β (Disj π β ((π β (π΄ β (β‘β― β {0, 1}))) βͺ (π β (π΄ β© (β‘β― β {0, 1}))))dom (π β I ) β Disj
π β (π β π΄)dom (π β I ))) |
161 | 153, 160 | mpbid 231 |
. 2
β’ (π β Disj π β (π β π΄)dom (π β I )) |
162 | 1, 2, 3, 8, 161 | symgcntz 31985 |
1
β’ (π β (π β π΄) β (πβ(π β π΄))) |