Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . . . 7
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β π β {π¦ β π« π· β£ π¦ β 2o}) |
2 | | breq1 5109 |
. . . . . . . 8
β’ (π¦ = π β (π¦ β 2o β π β
2o)) |
3 | 2 | elrab 3646 |
. . . . . . 7
β’ (π β {π¦ β π« π· β£ π¦ β 2o} β (π β π« π· β§ π β 2o)) |
4 | 1, 3 | sylib 217 |
. . . . . 6
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β (π β π« π· β§ π β 2o)) |
5 | 4 | simprd 497 |
. . . . 5
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β π β 2o) |
6 | | en2 9228 |
. . . . 5
β’ (π β 2o β
βπβπ π = {π, π}) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β βπβπ π = {π, π}) |
8 | 4 | simpld 496 |
. . . . . . . . . 10
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β π β π« π·) |
9 | 8 | elpwid 4570 |
. . . . . . . . 9
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β π β π·) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β π·) |
11 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
12 | 11 | prid1 4724 |
. . . . . . . . 9
β’ π β {π, π} |
13 | | simpr 486 |
. . . . . . . . 9
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π = {π, π}) |
14 | 12, 13 | eleqtrrid 2841 |
. . . . . . . 8
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β π) |
15 | 10, 14 | sseldd 3946 |
. . . . . . 7
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β π·) |
16 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
17 | 16 | prid2 4725 |
. . . . . . . . 9
β’ π β {π, π} |
18 | 17, 13 | eleqtrrid 2841 |
. . . . . . . 8
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β π) |
19 | 10, 18 | sseldd 3946 |
. . . . . . 7
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β π·) |
20 | 5 | adantr 482 |
. . . . . . . . . 10
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β 2o) |
21 | 13, 20 | eqbrtrrd 5130 |
. . . . . . . . 9
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β {π, π} β 2o) |
22 | | pr2ne 9945 |
. . . . . . . . . 10
β’ ((π β π· β§ π β π·) β ({π, π} β 2o β π β π)) |
23 | 22 | biimpa 478 |
. . . . . . . . 9
β’ (((π β π· β§ π β π·) β§ {π, π} β 2o) β π β π) |
24 | 15, 19, 21, 23 | syl21anc 837 |
. . . . . . . 8
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π β π) |
25 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) |
26 | | simp-4l 782 |
. . . . . . . . . . 11
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π· β π) |
27 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(pmTrspβπ·) =
(pmTrspβπ·) |
28 | 27 | pmtrval 19238 |
. . . . . . . . . . 11
β’ ((π· β π β§ π β π· β§ π β 2o) β
((pmTrspβπ·)βπ) = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) |
29 | 26, 10, 20, 28 | syl3anc 1372 |
. . . . . . . . . 10
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β ((pmTrspβπ·)βπ) = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) |
30 | 13 | fveq2d 6847 |
. . . . . . . . . 10
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β ((pmTrspβπ·)βπ) = ((pmTrspβπ·)β{π, π})) |
31 | 25, 29, 30 | 3eqtr2d 2779 |
. . . . . . . . 9
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π = ((pmTrspβπ·)β{π, π})) |
32 | | trsp2cyc.c |
. . . . . . . . . 10
β’ πΆ = (toCycβπ·) |
33 | 32, 26, 15, 19, 24, 27 | cycpm2tr 32017 |
. . . . . . . . 9
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β (πΆββ¨βππββ©) = ((pmTrspβπ·)β{π, π})) |
34 | 31, 33 | eqtr4d 2776 |
. . . . . . . 8
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β π = (πΆββ¨βππββ©)) |
35 | 24, 34 | jca 513 |
. . . . . . 7
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β (π β π β§ π = (πΆββ¨βππββ©))) |
36 | 15, 19, 35 | jca31 516 |
. . . . . 6
β’
(((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β§ π = {π, π}) β ((π β π· β§ π β π·) β§ (π β π β§ π = (πΆββ¨βππββ©)))) |
37 | 36 | ex 414 |
. . . . 5
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β (π = {π, π} β ((π β π· β§ π β π·) β§ (π β π β§ π = (πΆββ¨βππββ©))))) |
38 | 37 | 2eximdv 1923 |
. . . 4
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β (βπβπ π = {π, π} β βπβπ((π β π· β§ π β π·) β§ (π β π β§ π = (πΆββ¨βππββ©))))) |
39 | 7, 38 | mpd 15 |
. . 3
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β βπβπ((π β π· β§ π β π·) β§ (π β π β§ π = (πΆββ¨βππββ©)))) |
40 | | r2ex 3189 |
. . 3
β’
(βπ β
π· βπ β π· (π β π β§ π = (πΆββ¨βππββ©)) β βπβπ((π β π· β§ π β π·) β§ (π β π β§ π = (πΆββ¨βππββ©)))) |
41 | 39, 40 | sylibr 233 |
. 2
β’ ((((π· β π β§ π β π) β§ π β {π¦ β π« π· β£ π¦ β 2o}) β§ π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β βπ β π· βπ β π· (π β π β§ π = (πΆββ¨βππββ©))) |
42 | | simpr 486 |
. . . 4
β’ ((π· β π β§ π β π) β π β π) |
43 | | trsp2cyc.t |
. . . . 5
β’ π = ran (pmTrspβπ·) |
44 | 27 | pmtrfval 19237 |
. . . . . . 7
β’ (π· β π β (pmTrspβπ·) = (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
45 | 44 | adantr 482 |
. . . . . 6
β’ ((π· β π β§ π β π) β (pmTrspβπ·) = (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
46 | 45 | rneqd 5894 |
. . . . 5
β’ ((π· β π β§ π β π) β ran (pmTrspβπ·) = ran (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
47 | 43, 46 | eqtrid 2785 |
. . . 4
β’ ((π· β π β§ π β π) β π = ran (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
48 | 42, 47 | eleqtrd 2836 |
. . 3
β’ ((π· β π β§ π β π) β π β ran (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
49 | | eqid 2733 |
. . . . 5
β’ (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) = (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) |
50 | 49 | elrnmpt 5912 |
. . . 4
β’ (π β π β (π β ran (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β βπ β {π¦ β π« π· β£ π¦ β 2o}π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
51 | 50 | adantl 483 |
. . 3
β’ ((π· β π β§ π β π) β (π β ran (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) β βπ β {π¦ β π« π· β£ π¦ β 2o}π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) |
52 | 48, 51 | mpbid 231 |
. 2
β’ ((π· β π β§ π β π) β βπ β {π¦ β π« π· β£ π¦ β 2o}π = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) |
53 | 41, 52 | r19.29a 3156 |
1
β’ ((π· β π β§ π β π) β βπ β π· βπ β π· (π β π β§ π = (πΆββ¨βππββ©))) |