| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cyc3conja.c |
β’ πΆ = ( π β ( β‘ β― β { 3 } ) ) |
| 2 |
|
cyc3conja.a |
β’ π΄ = ( pmEven β π· ) |
| 3 |
|
cyc3conja.s |
β’ π = ( SymGrp β π· ) |
| 4 |
|
cyc3conja.n |
β’ π = ( β― β π· ) |
| 5 |
|
cyc3conja.m |
β’ π = ( toCyc β π· ) |
| 6 |
|
cyc3conja.p |
β’ + = ( +g β π ) |
| 7 |
|
cyc3conja.l |
β’ β = ( -g β π ) |
| 8 |
|
cyc3conja.1 |
β’ ( π β 5 β€ π ) |
| 9 |
|
cyc3conja.d |
β’ ( π β π· β Fin ) |
| 10 |
|
cyc3conja.q |
β’ ( π β π β πΆ ) |
| 11 |
|
cyc3conja.t |
β’ ( π β π β πΆ ) |
| 12 |
|
simpr |
β’ ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β π β π΄ ) |
| 13 |
|
simpr |
β’ ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β§ π = π ) β π = π ) |
| 14 |
13
|
oveq1d |
β’ ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β§ π = π ) β ( π + π ) = ( π + π ) ) |
| 15 |
14 13
|
oveq12d |
β’ ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β§ π = π ) β ( ( π + π ) β π ) = ( ( π + π ) β π ) ) |
| 16 |
15
|
eqeq2d |
β’ ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β§ π = π ) β ( π = ( ( π + π ) β π ) β π = ( ( π + π ) β π ) ) ) |
| 17 |
|
simplr |
β’ ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β π = ( ( π + π ) β π ) ) |
| 18 |
12 16 17
|
rspcedvd |
β’ ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ π β π΄ ) β β π β π΄ π = ( ( π + π ) β π ) ) |
| 19 |
9
|
ad5antr |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π· β Fin ) |
| 20 |
19
|
ad3antrrr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π· β Fin ) |
| 21 |
|
simp-8r |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π β ( Base β π ) ) |
| 22 |
|
simp-6r |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β Β¬ π β π΄ ) |
| 23 |
21 22
|
eldifd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π β ( ( Base β π ) β π΄ ) ) |
| 24 |
|
simpllr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π₯ β ( π· β ran π’ ) ) |
| 25 |
24
|
eldifad |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π₯ β π· ) |
| 26 |
|
simplr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π¦ β ( π· β ran π’ ) ) |
| 27 |
26
|
eldifad |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π¦ β π· ) |
| 28 |
25 27
|
prssd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β { π₯ , π¦ } β π· ) |
| 29 |
|
simpr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π₯ β π¦ ) |
| 30 |
|
enpr2 |
β’ ( ( π₯ β ( π· β ran π’ ) β§ π¦ β ( π· β ran π’ ) β§ π₯ β π¦ ) β { π₯ , π¦ } β 2o ) |
| 31 |
24 26 29 30
|
syl3anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β { π₯ , π¦ } β 2o ) |
| 32 |
|
eqid |
β’ ( pmTrsp β π· ) = ( pmTrsp β π· ) |
| 33 |
|
eqid |
β’ ran ( pmTrsp β π· ) = ran ( pmTrsp β π· ) |
| 34 |
32 33
|
pmtrrn |
β’ ( ( π· β Fin β§ { π₯ , π¦ } β π· β§ { π₯ , π¦ } β 2o ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ran ( pmTrsp β π· ) ) |
| 35 |
20 28 31 34
|
syl3anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ran ( pmTrsp β π· ) ) |
| 36 |
|
eqid |
β’ ( Base β π ) = ( Base β π ) |
| 37 |
3 36 33
|
pmtrodpm |
β’ ( ( π· β Fin β§ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ran ( pmTrsp β π· ) ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( ( Base β π ) β ( pmEven β π· ) ) ) |
| 38 |
20 35 37
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( ( Base β π ) β ( pmEven β π· ) ) ) |
| 39 |
2
|
difeq2i |
β’ ( ( Base β π ) β π΄ ) = ( ( Base β π ) β ( pmEven β π· ) ) |
| 40 |
38 39
|
eleqtrrdi |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( ( Base β π ) β π΄ ) ) |
| 41 |
3 36 2
|
odpmco |
β’ ( ( π· β Fin β§ π β ( ( Base β π ) β π΄ ) β§ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( ( Base β π ) β π΄ ) ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β π΄ ) |
| 42 |
20 23 40 41
|
syl3anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β π΄ ) |
| 43 |
|
simpr |
β’ ( ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β§ π = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β π = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 44 |
43
|
oveq1d |
β’ ( ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β§ π = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β ( π + π ) = ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) ) |
| 45 |
44 43
|
oveq12d |
β’ ( ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β§ π = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β ( ( π + π ) β π ) = ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) |
| 46 |
45
|
eqeq2d |
β’ ( ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β§ π = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β ( π = ( ( π + π ) β π ) β π = ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) ) |
| 47 |
38
|
eldifad |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( Base β π ) ) |
| 48 |
|
0zd |
β’ ( π β 0 β β€ ) |
| 49 |
|
hashcl |
β’ ( π· β Fin β ( β― β π· ) β β0 ) |
| 50 |
9 49
|
syl |
β’ ( π β ( β― β π· ) β β0 ) |
| 51 |
4 50
|
eqeltrid |
β’ ( π β π β β0 ) |
| 52 |
51
|
nn0zd |
β’ ( π β π β β€ ) |
| 53 |
|
3z |
β’ 3 β β€ |
| 54 |
53
|
a1i |
β’ ( π β 3 β β€ ) |
| 55 |
|
0red |
β’ ( π β 0 β β ) |
| 56 |
54
|
zred |
β’ ( π β 3 β β ) |
| 57 |
|
3pos |
β’ 0 < 3 |
| 58 |
57
|
a1i |
β’ ( π β 0 < 3 ) |
| 59 |
55 56 58
|
ltled |
β’ ( π β 0 β€ 3 ) |
| 60 |
|
5re |
β’ 5 β β |
| 61 |
60
|
a1i |
β’ ( π β 5 β β ) |
| 62 |
51
|
nn0red |
β’ ( π β π β β ) |
| 63 |
|
3lt5 |
β’ 3 < 5 |
| 64 |
63
|
a1i |
β’ ( π β 3 < 5 ) |
| 65 |
56 61 64
|
ltled |
β’ ( π β 3 β€ 5 ) |
| 66 |
56 61 62 65 8
|
letrd |
β’ ( π β 3 β€ π ) |
| 67 |
48 52 54 59 66
|
elfzd |
β’ ( π β 3 β ( 0 ... π ) ) |
| 68 |
1 3 4 5 36
|
cycpmgcl |
β’ ( ( π· β Fin β§ 3 β ( 0 ... π ) ) β πΆ β ( Base β π ) ) |
| 69 |
9 67 68
|
syl2anc |
β’ ( π β πΆ β ( Base β π ) ) |
| 70 |
69 11
|
sseldd |
β’ ( π β π β ( Base β π ) ) |
| 71 |
70
|
ad8antr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π β ( Base β π ) ) |
| 72 |
5 20 25 27 29 32
|
cycpm2tr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π β β¨β π₯ π¦ ββ© ) = ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) |
| 73 |
72
|
reseq1d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β β¨β π₯ π¦ ββ© ) βΎ ran π’ ) = ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) βΎ ran π’ ) ) |
| 74 |
25 27
|
s2cld |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β β¨β π₯ π¦ ββ© β Word π· ) |
| 75 |
25 27 29
|
s2f1 |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β β¨β π₯ π¦ ββ© : dom β¨β π₯ π¦ ββ© β1-1β π· ) |
| 76 |
5 20 74 75
|
tocycfvres2 |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β β¨β π₯ π¦ ββ© ) βΎ ( π· β ran β¨β π₯ π¦ ββ© ) ) = ( I βΎ ( π· β ran β¨β π₯ π¦ ββ© ) ) ) |
| 77 |
76
|
reseq1d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β β¨β π₯ π¦ ββ© ) βΎ ( π· β ran β¨β π₯ π¦ ββ© ) ) βΎ ran π’ ) = ( ( I βΎ ( π· β ran β¨β π₯ π¦ ββ© ) ) βΎ ran π’ ) ) |
| 78 |
|
simplr |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) |
| 79 |
78
|
elin1d |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π’ β { π€ β Word π· β£ π€ : dom π€ β1-1β π· } ) |
| 80 |
|
id |
β’ ( π€ = π’ β π€ = π’ ) |
| 81 |
|
dmeq |
β’ ( π€ = π’ β dom π€ = dom π’ ) |
| 82 |
|
eqidd |
β’ ( π€ = π’ β π· = π· ) |
| 83 |
80 81 82
|
f1eq123d |
β’ ( π€ = π’ β ( π€ : dom π€ β1-1β π· β π’ : dom π’ β1-1β π· ) ) |
| 84 |
83
|
elrab |
β’ ( π’ β { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β ( π’ β Word π· β§ π’ : dom π’ β1-1β π· ) ) |
| 85 |
79 84
|
sylib |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ( π’ β Word π· β§ π’ : dom π’ β1-1β π· ) ) |
| 86 |
85
|
simprd |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π’ : dom π’ β1-1β π· ) |
| 87 |
|
f1f |
β’ ( π’ : dom π’ β1-1β π· β π’ : dom π’ βΆ π· ) |
| 88 |
|
frn |
β’ ( π’ : dom π’ βΆ π· β ran π’ β π· ) |
| 89 |
86 87 88
|
3syl |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ran π’ β π· ) |
| 90 |
89
|
ad3antrrr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ran π’ β π· ) |
| 91 |
24 26
|
prssd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β { π₯ , π¦ } β ( π· β ran π’ ) ) |
| 92 |
|
ssconb |
β’ ( ( { π₯ , π¦ } β π· β§ ran π’ β π· ) β ( { π₯ , π¦ } β ( π· β ran π’ ) β ran π’ β ( π· β { π₯ , π¦ } ) ) ) |
| 93 |
92
|
biimpa |
β’ ( ( ( { π₯ , π¦ } β π· β§ ran π’ β π· ) β§ { π₯ , π¦ } β ( π· β ran π’ ) ) β ran π’ β ( π· β { π₯ , π¦ } ) ) |
| 94 |
28 90 91 93
|
syl21anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ran π’ β ( π· β { π₯ , π¦ } ) ) |
| 95 |
24 26
|
s2rn |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ran β¨β π₯ π¦ ββ© = { π₯ , π¦ } ) |
| 96 |
95
|
difeq2d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π· β ran β¨β π₯ π¦ ββ© ) = ( π· β { π₯ , π¦ } ) ) |
| 97 |
94 96
|
sseqtrrd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ran π’ β ( π· β ran β¨β π₯ π¦ ββ© ) ) |
| 98 |
97
|
resabs1d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β β¨β π₯ π¦ ββ© ) βΎ ( π· β ran β¨β π₯ π¦ ββ© ) ) βΎ ran π’ ) = ( ( π β β¨β π₯ π¦ ββ© ) βΎ ran π’ ) ) |
| 99 |
97
|
resabs1d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( I βΎ ( π· β ran β¨β π₯ π¦ ββ© ) ) βΎ ran π’ ) = ( I βΎ ran π’ ) ) |
| 100 |
77 98 99
|
3eqtr3d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β β¨β π₯ π¦ ββ© ) βΎ ran π’ ) = ( I βΎ ran π’ ) ) |
| 101 |
73 100
|
eqtr3d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) βΎ ran π’ ) = ( I βΎ ran π’ ) ) |
| 102 |
|
simp-4r |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π β π’ ) = π ) |
| 103 |
102
|
reseq1d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β π’ ) βΎ ( π· β ran π’ ) ) = ( π βΎ ( π· β ran π’ ) ) ) |
| 104 |
85
|
simpld |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π’ β Word π· ) |
| 105 |
104
|
ad3antrrr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π’ β Word π· ) |
| 106 |
86
|
ad3antrrr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π’ : dom π’ β1-1β π· ) |
| 107 |
5 20 105 106
|
tocycfvres2 |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β π’ ) βΎ ( π· β ran π’ ) ) = ( I βΎ ( π· β ran π’ ) ) ) |
| 108 |
103 107
|
eqtr3d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π βΎ ( π· β ran π’ ) ) = ( I βΎ ( π· β ran π’ ) ) ) |
| 109 |
|
disjdif |
β’ ( ran π’ β© ( π· β ran π’ ) ) = β
|
| 110 |
109
|
a1i |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ran π’ β© ( π· β ran π’ ) ) = β
) |
| 111 |
|
undif |
β’ ( ran π’ β π· β ( ran π’ βͺ ( π· β ran π’ ) ) = π· ) |
| 112 |
90 111
|
sylib |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ran π’ βͺ ( π· β ran π’ ) ) = π· ) |
| 113 |
3 36 47 71 101 108 110 112
|
symgcom |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β π ) = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 114 |
113
|
coeq2d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β π ) ) = ( π β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) |
| 115 |
3 36 6
|
symgov |
β’ ( ( π β ( Base β π ) β§ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( Base β π ) ) β ( π + ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 116 |
21 47 115
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π + ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 117 |
3 36 6
|
symgcl |
β’ ( ( π β ( Base β π ) β§ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( Base β π ) ) β ( π + ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( Base β π ) ) |
| 118 |
21 47 117
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π + ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( Base β π ) ) |
| 119 |
116 118
|
eqeltrrd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( Base β π ) ) |
| 120 |
3 36 6
|
symgov |
β’ ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( Base β π ) β§ π β ( Base β π ) ) β ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) = ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β π ) ) |
| 121 |
119 71 120
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) = ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β π ) ) |
| 122 |
|
coass |
β’ ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β π ) = ( π β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β π ) ) |
| 123 |
121 122
|
eqtrdi |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) = ( π β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β π ) ) ) |
| 124 |
|
coass |
β’ ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( π β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 125 |
124
|
a1i |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( π β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) |
| 126 |
114 123 125
|
3eqtr4d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) = ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 127 |
|
cnvco |
β’ β‘ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ π ) |
| 128 |
127
|
a1i |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β β‘ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ π ) ) |
| 129 |
126 128
|
coeq12d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β β‘ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) = ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ π ) ) ) |
| 130 |
|
coass |
β’ ( ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β β‘ π ) = ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ π ) ) |
| 131 |
|
coass |
β’ ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) |
| 132 |
131
|
coeq1i |
β’ ( ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β β‘ π ) = ( ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β β‘ π ) |
| 133 |
130 132
|
eqtr3i |
β’ ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ π ) ) = ( ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β β‘ π ) |
| 134 |
133
|
a1i |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ π ) ) = ( ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β β‘ π ) ) |
| 135 |
3 36 6
|
symgov |
β’ ( ( π β ( Base β π ) β§ π β ( Base β π ) ) β ( π + π ) = ( π β π ) ) |
| 136 |
21 71 135
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π + π ) = ( π β π ) ) |
| 137 |
3 36 6
|
symgcl |
β’ ( ( π β ( Base β π ) β§ π β ( Base β π ) ) β ( π + π ) β ( Base β π ) ) |
| 138 |
21 71 137
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π + π ) β ( Base β π ) ) |
| 139 |
136 138
|
eqeltrrd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( π β π ) β ( Base β π ) ) |
| 140 |
3 36
|
symgbasf |
β’ ( ( π β π ) β ( Base β π ) β ( π β π ) : π· βΆ π· ) |
| 141 |
|
fcoi1 |
β’ ( ( π β π ) : π· βΆ π· β ( ( π β π ) β ( I βΎ π· ) ) = ( π β π ) ) |
| 142 |
139 140 141
|
3syl |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β π ) β ( I βΎ π· ) ) = ( π β π ) ) |
| 143 |
3 36
|
elsymgbas |
β’ ( π· β Fin β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( Base β π ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) : π· β1-1-ontoβ π· ) ) |
| 144 |
143
|
biimpa |
β’ ( ( π· β Fin β§ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β ( Base β π ) ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) : π· β1-1-ontoβ π· ) |
| 145 |
20 47 144
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) : π· β1-1-ontoβ π· ) |
| 146 |
|
f1ococnv2 |
β’ ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) : π· β1-1-ontoβ π· β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( I βΎ π· ) ) |
| 147 |
145 146
|
syl |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) = ( I βΎ π· ) ) |
| 148 |
147
|
coeq2d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) = ( ( π β π ) β ( I βΎ π· ) ) ) |
| 149 |
142 148 136
|
3eqtr4d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) = ( π + π ) ) |
| 150 |
149
|
coeq1d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β β‘ π ) = ( ( π + π ) β β‘ π ) ) |
| 151 |
3 36 7
|
symgsubg |
β’ ( ( ( π + π ) β ( Base β π ) β§ π β ( Base β π ) ) β ( ( π + π ) β π ) = ( ( π + π ) β β‘ π ) ) |
| 152 |
138 21 151
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π + π ) β π ) = ( ( π + π ) β β‘ π ) ) |
| 153 |
150 152
|
eqtr4d |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β π ) β ( ( ( pmTrsp β π· ) β { π₯ , π¦ } ) β β‘ ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) β β‘ π ) = ( ( π + π ) β π ) ) |
| 154 |
129 134 153
|
3eqtrd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β β‘ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) = ( ( π + π ) β π ) ) |
| 155 |
3
|
symggrp |
β’ ( π· β Fin β π β Grp ) |
| 156 |
9 155
|
syl |
β’ ( π β π β Grp ) |
| 157 |
156
|
ad8antr |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π β Grp ) |
| 158 |
36 6
|
grpcl |
β’ ( ( π β Grp β§ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( Base β π ) β§ π β ( Base β π ) ) β ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( Base β π ) ) |
| 159 |
157 119 71 158
|
syl3anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( Base β π ) ) |
| 160 |
3 36 7
|
symgsubg |
β’ ( ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( Base β π ) β§ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) β ( Base β π ) ) β ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) = ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β β‘ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) |
| 161 |
159 119 160
|
syl2anc |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) = ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β β‘ ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) |
| 162 |
|
simp-7r |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π = ( ( π + π ) β π ) ) |
| 163 |
154 161 162
|
3eqtr4rd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β π = ( ( ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) + π ) β ( π β ( ( pmTrsp β π· ) β { π₯ , π¦ } ) ) ) ) |
| 164 |
42 46 163
|
rspcedvd |
β’ ( ( ( ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β§ π₯ β ( π· β ran π’ ) ) β§ π¦ β ( π· β ran π’ ) ) β§ π₯ β π¦ ) β β π β π΄ π = ( ( π + π ) β π ) ) |
| 165 |
9
|
difexd |
β’ ( π β ( π· β ran π’ ) β V ) |
| 166 |
165
|
ad5antr |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ( π· β ran π’ ) β V ) |
| 167 |
|
3p2e5 |
β’ ( 3 + 2 ) = 5 |
| 168 |
167 8
|
eqbrtrid |
β’ ( π β ( 3 + 2 ) β€ π ) |
| 169 |
|
2re |
β’ 2 β β |
| 170 |
169
|
a1i |
β’ ( π β 2 β β ) |
| 171 |
56 170 62
|
leaddsub2d |
β’ ( π β ( ( 3 + 2 ) β€ π β 2 β€ ( π β 3 ) ) ) |
| 172 |
168 171
|
mpbid |
β’ ( π β 2 β€ ( π β 3 ) ) |
| 173 |
172
|
ad5antr |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β 2 β€ ( π β 3 ) ) |
| 174 |
4
|
a1i |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π = ( β― β π· ) ) |
| 175 |
78
|
elin2d |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β π’ β ( β‘ β― β { 3 } ) ) |
| 176 |
|
hashf |
β’ β― : V βΆ ( β0 βͺ { +β } ) |
| 177 |
|
ffn |
β’ ( β― : V βΆ ( β0 βͺ { +β } ) β β― Fn V ) |
| 178 |
|
fniniseg |
β’ ( β― Fn V β ( π’ β ( β‘ β― β { 3 } ) β ( π’ β V β§ ( β― β π’ ) = 3 ) ) ) |
| 179 |
176 177 178
|
mp2b |
β’ ( π’ β ( β‘ β― β { 3 } ) β ( π’ β V β§ ( β― β π’ ) = 3 ) ) |
| 180 |
179
|
simprbi |
β’ ( π’ β ( β‘ β― β { 3 } ) β ( β― β π’ ) = 3 ) |
| 181 |
175 180
|
syl |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ( β― β π’ ) = 3 ) |
| 182 |
|
vex |
β’ π’ β V |
| 183 |
182
|
dmex |
β’ dom π’ β V |
| 184 |
|
hashf1rn |
β’ ( ( dom π’ β V β§ π’ : dom π’ β1-1β π· ) β ( β― β π’ ) = ( β― β ran π’ ) ) |
| 185 |
183 86 184
|
sylancr |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ( β― β π’ ) = ( β― β ran π’ ) ) |
| 186 |
181 185
|
eqtr3d |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β 3 = ( β― β ran π’ ) ) |
| 187 |
174 186
|
oveq12d |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ( π β 3 ) = ( ( β― β π· ) β ( β― β ran π’ ) ) ) |
| 188 |
173 187
|
breqtrd |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β 2 β€ ( ( β― β π· ) β ( β― β ran π’ ) ) ) |
| 189 |
|
hashssdif |
β’ ( ( π· β Fin β§ ran π’ β π· ) β ( β― β ( π· β ran π’ ) ) = ( ( β― β π· ) β ( β― β ran π’ ) ) ) |
| 190 |
19 89 189
|
syl2anc |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β ( β― β ( π· β ran π’ ) ) = ( ( β― β π· ) β ( β― β ran π’ ) ) ) |
| 191 |
188 190
|
breqtrrd |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β 2 β€ ( β― β ( π· β ran π’ ) ) ) |
| 192 |
|
hashge2el2dif |
β’ ( ( ( π· β ran π’ ) β V β§ 2 β€ ( β― β ( π· β ran π’ ) ) ) β β π₯ β ( π· β ran π’ ) β π¦ β ( π· β ran π’ ) π₯ β π¦ ) |
| 193 |
166 191 192
|
syl2anc |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β β π₯ β ( π· β ran π’ ) β π¦ β ( π· β ran π’ ) π₯ β π¦ ) |
| 194 |
164 193
|
r19.29vva |
β’ ( ( ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β§ π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ) β§ ( π β π’ ) = π ) β β π β π΄ π = ( ( π + π ) β π ) ) |
| 195 |
|
nfcv |
β’ β² π’ π |
| 196 |
5 3 36
|
tocycf |
β’ ( π· β Fin β π : { π€ β Word π· β£ π€ : dom π€ β1-1β π· } βΆ ( Base β π ) ) |
| 197 |
|
ffn |
β’ ( π : { π€ β Word π· β£ π€ : dom π€ β1-1β π· } βΆ ( Base β π ) β π Fn { π€ β Word π· β£ π€ : dom π€ β1-1β π· } ) |
| 198 |
9 196 197
|
3syl |
β’ ( π β π Fn { π€ β Word π· β£ π€ : dom π€ β1-1β π· } ) |
| 199 |
11 1
|
eleqtrdi |
β’ ( π β π β ( π β ( β‘ β― β { 3 } ) ) ) |
| 200 |
195 198 199
|
fvelimad |
β’ ( π β β π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ( π β π’ ) = π ) |
| 201 |
200
|
ad3antrrr |
β’ ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β β π’ β ( { π€ β Word π· β£ π€ : dom π€ β1-1β π· } β© ( β‘ β― β { 3 } ) ) ( π β π’ ) = π ) |
| 202 |
194 201
|
r19.29a |
β’ ( ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β§ Β¬ π β π΄ ) β β π β π΄ π = ( ( π + π ) β π ) ) |
| 203 |
18 202
|
pm2.61dan |
β’ ( ( ( π β§ π β ( Base β π ) ) β§ π = ( ( π + π ) β π ) ) β β π β π΄ π = ( ( π + π ) β π ) ) |
| 204 |
1 3 4 5 36 6 7 67 9 10 11
|
cycpmconjs |
β’ ( π β β π β ( Base β π ) π = ( ( π + π ) β π ) ) |
| 205 |
203 204
|
r19.29a |
β’ ( π β β π β π΄ π = ( ( π + π ) β π ) ) |