Proof of Theorem metideq
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . 5
PsMet ~Met ~Met
PsMet |
2 | | metidss 29934 |
. . . . . . . . 9
PsMet
~Met
|
3 | | dmss 5323 |
. . . . . . . . 9
~Met ~Met |
4 | 2, 3 | syl 17 |
. . . . . . . 8
PsMet
~Met
|
5 | | dmxpid 5345 |
. . . . . . . 8
|
6 | 4, 5 | syl6sseq 3651 |
. . . . . . 7
PsMet
~Met |
7 | 1, 6 | syl 17 |
. . . . . 6
PsMet ~Met ~Met
~Met |
8 | | xpss 5226 |
. . . . . . . . . 10
|
9 | 2, 8 | syl6ss 3615 |
. . . . . . . . 9
PsMet
~Met
|
10 | | df-rel 5121 |
. . . . . . . . 9
~Met ~Met |
11 | 9, 10 | sylibr 224 |
. . . . . . . 8
PsMet
~Met |
12 | 1, 11 | syl 17 |
. . . . . . 7
PsMet ~Met ~Met
~Met |
13 | | simprl 794 |
. . . . . . 7
PsMet ~Met ~Met
~Met |
14 | | releldm 5358 |
. . . . . . 7
~Met
~Met ~Met |
15 | 12, 13, 14 | syl2anc 693 |
. . . . . 6
PsMet ~Met ~Met
~Met |
16 | 7, 15 | sseldd 3604 |
. . . . 5
PsMet ~Met ~Met
|
17 | | simprr 796 |
. . . . . . 7
PsMet ~Met ~Met
~Met |
18 | | releldm 5358 |
. . . . . . 7
~Met
~Met ~Met |
19 | 12, 17, 18 | syl2anc 693 |
. . . . . 6
PsMet ~Met ~Met
~Met |
20 | 7, 19 | sseldd 3604 |
. . . . 5
PsMet ~Met ~Met
|
21 | | psmetsym 22115 |
. . . . 5
PsMet
|
22 | 1, 16, 20, 21 | syl3anc 1326 |
. . . 4
PsMet ~Met ~Met
|
23 | | psmetf 22111 |
. . . . . 6
PsMet
|
24 | 23 | fovrnda 6805 |
. . . . 5
PsMet
|
25 | 1, 20, 16, 24 | syl12anc 1324 |
. . . 4
PsMet ~Met ~Met
|
26 | 22, 25 | eqeltrd 2701 |
. . 3
PsMet ~Met ~Met
|
27 | | rnss 5354 |
. . . . . . . 8
~Met ~Met |
28 | 2, 27 | syl 17 |
. . . . . . 7
PsMet
~Met
|
29 | | rnxpid 5567 |
. . . . . . 7
|
30 | 28, 29 | syl6sseq 3651 |
. . . . . 6
PsMet
~Met |
31 | 1, 30 | syl 17 |
. . . . 5
PsMet ~Met ~Met
~Met |
32 | | relelrn 5359 |
. . . . . 6
~Met
~Met ~Met |
33 | 12, 13, 32 | syl2anc 693 |
. . . . 5
PsMet ~Met ~Met
~Met |
34 | 31, 33 | sseldd 3604 |
. . . 4
PsMet ~Met ~Met
|
35 | 23 | fovrnda 6805 |
. . . 4
PsMet
|
36 | 1, 34, 20, 35 | syl12anc 1324 |
. . 3
PsMet ~Met ~Met
|
37 | | relelrn 5359 |
. . . . . . 7
~Met
~Met ~Met |
38 | 12, 17, 37 | syl2anc 693 |
. . . . . 6
PsMet ~Met ~Met
~Met |
39 | 31, 38 | sseldd 3604 |
. . . . 5
PsMet ~Met ~Met
|
40 | | psmetsym 22115 |
. . . . 5
PsMet
|
41 | 1, 39, 34, 40 | syl3anc 1326 |
. . . 4
PsMet ~Met ~Met
|
42 | 23 | fovrnda 6805 |
. . . . 5
PsMet
|
43 | 1, 39, 34, 42 | syl12anc 1324 |
. . . 4
PsMet ~Met ~Met
|
44 | 41, 43 | eqeltrrd 2702 |
. . 3
PsMet ~Met ~Met
|
45 | | psmettri2 22114 |
. . . . 5
PsMet
|
46 | 1, 34, 16, 20, 45 | syl13anc 1328 |
. . . 4
PsMet ~Met ~Met
|
47 | | psmetsym 22115 |
. . . . . . . 8
PsMet
|
48 | 1, 16, 34, 47 | syl3anc 1326 |
. . . . . . 7
PsMet ~Met ~Met
|
49 | 16, 34 | jca 554 |
. . . . . . . 8
PsMet ~Met ~Met
|
50 | | metidv 29935 |
. . . . . . . . 9
PsMet
~Met |
51 | 50 | biimpa 501 |
. . . . . . . 8
PsMet
~Met |
52 | 1, 49, 13, 51 | syl21anc 1325 |
. . . . . . 7
PsMet ~Met ~Met
|
53 | 48, 52 | eqtr3d 2658 |
. . . . . 6
PsMet ~Met ~Met
|
54 | 53 | oveq1d 6665 |
. . . . 5
PsMet ~Met ~Met
|
55 | | xaddid2 12073 |
. . . . . 6
|
56 | 36, 55 | syl 17 |
. . . . 5
PsMet ~Met ~Met
|
57 | 54, 56 | eqtrd 2656 |
. . . 4
PsMet ~Met ~Met
|
58 | 46, 57 | breqtrd 4679 |
. . 3
PsMet ~Met ~Met
|
59 | | psmettri2 22114 |
. . . . 5
PsMet
|
60 | 1, 39, 34, 20, 59 | syl13anc 1328 |
. . . 4
PsMet ~Met ~Met
|
61 | | psmetsym 22115 |
. . . . . . . 8
PsMet
|
62 | 1, 39, 20, 61 | syl3anc 1326 |
. . . . . . 7
PsMet ~Met ~Met
|
63 | 20, 39 | jca 554 |
. . . . . . . 8
PsMet ~Met ~Met
|
64 | | metidv 29935 |
. . . . . . . . 9
PsMet
~Met |
65 | 64 | biimpa 501 |
. . . . . . . 8
PsMet
~Met |
66 | 1, 63, 17, 65 | syl21anc 1325 |
. . . . . . 7
PsMet ~Met ~Met
|
67 | 62, 66 | eqtrd 2656 |
. . . . . 6
PsMet ~Met ~Met
|
68 | 67 | oveq2d 6666 |
. . . . 5
PsMet ~Met ~Met
|
69 | | xaddid1 12072 |
. . . . . 6
|
70 | 43, 69 | syl 17 |
. . . . 5
PsMet ~Met ~Met
|
71 | 68, 70, 41 | 3eqtrd 2660 |
. . . 4
PsMet ~Met ~Met
|
72 | 60, 71 | breqtrd 4679 |
. . 3
PsMet ~Met ~Met
|
73 | 26, 36, 44, 58, 72 | xrletrd 11993 |
. 2
PsMet ~Met ~Met
|
74 | 23 | fovrnda 6805 |
. . . 4
PsMet
|
75 | 1, 16, 39, 74 | syl12anc 1324 |
. . 3
PsMet ~Met ~Met
|
76 | | psmettri2 22114 |
. . . . 5
PsMet
|
77 | 1, 16, 34, 39, 76 | syl13anc 1328 |
. . . 4
PsMet ~Met ~Met
|
78 | 52 | oveq1d 6665 |
. . . . 5
PsMet ~Met ~Met
|
79 | | xaddid2 12073 |
. . . . . 6
|
80 | 75, 79 | syl 17 |
. . . . 5
PsMet ~Met ~Met
|
81 | 78, 80 | eqtrd 2656 |
. . . 4
PsMet ~Met ~Met
|
82 | 77, 81 | breqtrd 4679 |
. . 3
PsMet ~Met ~Met
|
83 | | psmettri2 22114 |
. . . . 5
PsMet
|
84 | 1, 20, 16, 39, 83 | syl13anc 1328 |
. . . 4
PsMet ~Met ~Met
|
85 | | xaddid1 12072 |
. . . . . 6
|
86 | 25, 85 | syl 17 |
. . . . 5
PsMet ~Met ~Met
|
87 | 66 | oveq2d 6666 |
. . . . 5
PsMet ~Met ~Met
|
88 | 86, 87, 22 | 3eqtr4d 2666 |
. . . 4
PsMet ~Met ~Met
|
89 | 84, 88 | breqtrd 4679 |
. . 3
PsMet ~Met ~Met
|
90 | 44, 75, 26, 82, 89 | xrletrd 11993 |
. 2
PsMet ~Met ~Met
|
91 | | xrletri3 11985 |
. . 3
|
92 | 26, 44, 91 | syl2anc 693 |
. 2
PsMet ~Met ~Met
|
93 | 73, 90, 92 | mpbir2and 957 |
1
PsMet ~Met ~Met
|