Step | Hyp | Ref
| Expression |
1 | | metidss 29934 |
. . . 4
PsMet
~Met
|
2 | | xpss 5226 |
. . . 4
|
3 | 1, 2 | syl6ss 3615 |
. . 3
PsMet
~Met
|
4 | | df-rel 5121 |
. . 3
~Met ~Met |
5 | 3, 4 | sylibr 224 |
. 2
PsMet
~Met |
6 | 1 | ssbrd 4696 |
. . . . 5
PsMet
~Met
|
7 | 6 | imp 445 |
. . . 4
PsMet ~Met |
8 | | brxp 5147 |
. . . 4
|
9 | 7, 8 | sylib 208 |
. . 3
PsMet ~Met
|
10 | | psmetsym 22115 |
. . . . . . . 8
PsMet
|
11 | 10 | 3expb 1266 |
. . . . . . 7
PsMet
|
12 | 11 | eqeq1d 2624 |
. . . . . 6
PsMet
|
13 | | metidv 29935 |
. . . . . 6
PsMet
~Met |
14 | | metidv 29935 |
. . . . . . 7
PsMet
~Met |
15 | 14 | ancom2s 844 |
. . . . . 6
PsMet
~Met |
16 | 12, 13, 15 | 3bitr4d 300 |
. . . . 5
PsMet
~Met ~Met |
17 | 16 | biimpd 219 |
. . . 4
PsMet
~Met
~Met |
18 | 17 | impancom 456 |
. . 3
PsMet ~Met
~Met |
19 | 9, 18 | mpd 15 |
. 2
PsMet ~Met ~Met |
20 | | simpl 473 |
. . . . . 6
PsMet ~Met ~Met
PsMet |
21 | | simprr 796 |
. . . . . . . 8
PsMet ~Met ~Met ~Met |
22 | 1 | ssbrd 4696 |
. . . . . . . . . 10
PsMet
~Met
|
23 | 22 | imp 445 |
. . . . . . . . 9
PsMet ~Met |
24 | | brxp 5147 |
. . . . . . . . 9
|
25 | 23, 24 | sylib 208 |
. . . . . . . 8
PsMet ~Met
|
26 | 21, 25 | syldan 487 |
. . . . . . 7
PsMet ~Met ~Met
|
27 | 26 | simpld 475 |
. . . . . 6
PsMet ~Met ~Met |
28 | | simprl 794 |
. . . . . . . 8
PsMet ~Met ~Met ~Met |
29 | 28, 9 | syldan 487 |
. . . . . . 7
PsMet ~Met ~Met
|
30 | 29 | simpld 475 |
. . . . . 6
PsMet ~Met ~Met
|
31 | 26 | simprd 479 |
. . . . . 6
PsMet ~Met ~Met |
32 | | psmettri2 22114 |
. . . . . 6
PsMet
|
33 | 20, 27, 30, 31, 32 | syl13anc 1328 |
. . . . 5
PsMet ~Met ~Met
|
34 | 29, 11 | syldan 487 |
. . . . . . . 8
PsMet ~Met ~Met |
35 | 29, 13 | syldan 487 |
. . . . . . . . 9
PsMet ~Met ~Met ~Met
|
36 | 28, 35 | mpbid 222 |
. . . . . . . 8
PsMet ~Met ~Met |
37 | 34, 36 | eqtr3d 2658 |
. . . . . . 7
PsMet ~Met ~Met |
38 | | metidv 29935 |
. . . . . . . . 9
PsMet
~Met |
39 | 26, 38 | syldan 487 |
. . . . . . . 8
PsMet ~Met ~Met ~Met
|
40 | 21, 39 | mpbid 222 |
. . . . . . 7
PsMet ~Met ~Met |
41 | 37, 40 | oveq12d 6668 |
. . . . . 6
PsMet ~Met ~Met |
42 | | 0xr 10086 |
. . . . . . 7
|
43 | | xaddid1 12072 |
. . . . . . 7
|
44 | 42, 43 | ax-mp 5 |
. . . . . 6
|
45 | 41, 44 | syl6eq 2672 |
. . . . 5
PsMet ~Met ~Met |
46 | 33, 45 | breqtrd 4679 |
. . . 4
PsMet ~Met ~Met
|
47 | | psmetge0 22117 |
. . . . 5
PsMet
|
48 | 20, 30, 31, 47 | syl3anc 1326 |
. . . 4
PsMet ~Met ~Met
|
49 | | psmetcl 22112 |
. . . . . 6
PsMet
|
50 | 20, 30, 31, 49 | syl3anc 1326 |
. . . . 5
PsMet ~Met ~Met |
51 | | xrletri3 11985 |
. . . . 5
|
52 | 50, 42, 51 | sylancl 694 |
. . . 4
PsMet ~Met ~Met
|
53 | 46, 48, 52 | mpbir2and 957 |
. . 3
PsMet ~Met ~Met |
54 | | metidv 29935 |
. . . 4
PsMet
~Met |
55 | 20, 30, 31, 54 | syl12anc 1324 |
. . 3
PsMet ~Met ~Met ~Met
|
56 | 53, 55 | mpbird 247 |
. 2
PsMet ~Met ~Met ~Met |
57 | | psmet0 22113 |
. . . 4
PsMet |
58 | | metidv 29935 |
. . . . 5
PsMet
~Met |
59 | 58 | anabsan2 863 |
. . . 4
PsMet ~Met
|
60 | 57, 59 | mpbird 247 |
. . 3
PsMet ~Met |
61 | 1 | ssbrd 4696 |
. . . . . 6
PsMet
~Met
|
62 | 61 | imp 445 |
. . . . 5
PsMet ~Met |
63 | | brxp 5147 |
. . . . 5
|
64 | 62, 63 | sylib 208 |
. . . 4
PsMet ~Met
|
65 | 64 | simpld 475 |
. . 3
PsMet ~Met |
66 | 60, 65 | impbida 877 |
. 2
PsMet
~Met |
67 | 5, 19, 56, 66 | iserd 7768 |
1
PsMet
~Met |