Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
|
2 | | vex 3203 |
. . . . . . 7
|
3 | | vex 3203 |
. . . . . . 7
|
4 | 2, 3 | ab2rexex 7159 |
. . . . . 6
|
5 | 4 | uniex 6953 |
. . . . 5
|
6 | 1, 5 | fnmpt2i 7239 |
. . . 4
|
7 | | pstmval.1 |
. . . . . 6
~Met |
8 | 7 | pstmval 29938 |
. . . . 5
PsMet
pstoMet
|
9 | 8 | fneq1d 5981 |
. . . 4
PsMet
pstoMet
|
10 | 6, 9 | mpbiri 248 |
. . 3
PsMet
pstoMet |
11 | | simpllr 799 |
. . . . . . . . 9
PsMet
|
12 | | simpr 477 |
. . . . . . . . 9
PsMet
|
13 | 11, 12 | oveq12d 6668 |
. . . . . . . 8
PsMet
pstoMet pstoMet |
14 | | simp-5l 808 |
. . . . . . . . 9
PsMet
PsMet |
15 | | simp-4r 807 |
. . . . . . . . 9
PsMet
|
16 | | simplr 792 |
. . . . . . . . 9
PsMet
|
17 | 7 | pstmfval 29939 |
. . . . . . . . 9
PsMet
pstoMet |
18 | 14, 15, 16, 17 | syl3anc 1326 |
. . . . . . . 8
PsMet
pstoMet |
19 | 13, 18 | eqtrd 2656 |
. . . . . . 7
PsMet
pstoMet |
20 | | psmetf 22111 |
. . . . . . . . 9
PsMet
|
21 | 14, 20 | syl 17 |
. . . . . . . 8
PsMet
|
22 | 21, 15, 16 | fovrnd 6806 |
. . . . . . 7
PsMet
|
23 | 19, 22 | eqeltrd 2701 |
. . . . . 6
PsMet
pstoMet |
24 | | elqsi 7800 |
. . . . . . . 8
|
25 | 24 | ad2antll 765 |
. . . . . . 7
PsMet
|
26 | 25 | ad2antrr 762 |
. . . . . 6
PsMet
|
27 | 23, 26 | r19.29a 3078 |
. . . . 5
PsMet
pstoMet |
28 | | elqsi 7800 |
. . . . . 6
|
29 | 28 | ad2antrl 764 |
. . . . 5
PsMet
|
30 | 27, 29 | r19.29a 3078 |
. . . 4
PsMet
pstoMet |
31 | 30 | ralrimivva 2971 |
. . 3
PsMet
pstoMet |
32 | | ffnov 6764 |
. . 3
pstoMet
pstoMet
pstoMet |
33 | 10, 31, 32 | sylanbrc 698 |
. 2
PsMet
pstoMet |
34 | 17 | 3expa 1265 |
. . . . . . . . . . . 12
PsMet pstoMet |
35 | 34 | eqeq1d 2624 |
. . . . . . . . . . 11
PsMet pstoMet |
36 | 7 | breqi 4659 |
. . . . . . . . . . . 12
~Met |
37 | | metidv 29935 |
. . . . . . . . . . . . 13
PsMet
~Met |
38 | 37 | anassrs 680 |
. . . . . . . . . . . 12
PsMet ~Met
|
39 | 36, 38 | syl5bb 272 |
. . . . . . . . . . 11
PsMet
|
40 | | metider 29937 |
. . . . . . . . . . . . . 14
PsMet
~Met |
41 | 40 | ad2antrr 762 |
. . . . . . . . . . . . 13
PsMet ~Met |
42 | | ereq1 7749 |
. . . . . . . . . . . . . 14
~Met ~Met |
43 | 7, 42 | ax-mp 5 |
. . . . . . . . . . . . 13
~Met |
44 | 41, 43 | sylibr 224 |
. . . . . . . . . . . 12
PsMet |
45 | | simplr 792 |
. . . . . . . . . . . 12
PsMet |
46 | 44, 45 | erth 7791 |
. . . . . . . . . . 11
PsMet
|
47 | 35, 39, 46 | 3bitr2d 296 |
. . . . . . . . . 10
PsMet pstoMet |
48 | 47 | adantllr 755 |
. . . . . . . . 9
PsMet
pstoMet |
49 | 48 | adantlr 751 |
. . . . . . . 8
PsMet
pstoMet
|
50 | 49 | adantr 481 |
. . . . . . 7
PsMet
pstoMet |
51 | 13 | eqeq1d 2624 |
. . . . . . 7
PsMet
pstoMet pstoMet |
52 | 11, 12 | eqeq12d 2637 |
. . . . . . 7
PsMet
|
53 | 50, 51, 52 | 3bitr4d 300 |
. . . . . 6
PsMet
pstoMet |
54 | 53, 26 | r19.29a 3078 |
. . . . 5
PsMet
pstoMet |
55 | 54, 29 | r19.29a 3078 |
. . . 4
PsMet
pstoMet |
56 | | simp-6l 810 |
. . . . . . . . . . . . . 14
PsMet
PsMet |
57 | | simplr 792 |
. . . . . . . . . . . . . 14
PsMet
|
58 | | simp-6r 811 |
. . . . . . . . . . . . . 14
PsMet
|
59 | | simp-4r 807 |
. . . . . . . . . . . . . 14
PsMet
|
60 | | psmettri2 22114 |
. . . . . . . . . . . . . 14
PsMet
|
61 | 56, 57, 58, 59, 60 | syl13anc 1328 |
. . . . . . . . . . . . 13
PsMet
|
62 | | simp-5r 809 |
. . . . . . . . . . . . . . 15
PsMet
|
63 | | simpllr 799 |
. . . . . . . . . . . . . . 15
PsMet
|
64 | 62, 63 | oveq12d 6668 |
. . . . . . . . . . . . . 14
PsMet
pstoMet pstoMet |
65 | 56, 58, 59, 17 | syl3anc 1326 |
. . . . . . . . . . . . . 14
PsMet
pstoMet |
66 | 64, 65 | eqtrd 2656 |
. . . . . . . . . . . . 13
PsMet
pstoMet |
67 | | simpr 477 |
. . . . . . . . . . . . . . . 16
PsMet
|
68 | 67, 62 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
PsMet
pstoMet pstoMet |
69 | 7 | pstmfval 29939 |
. . . . . . . . . . . . . . . 16
PsMet
pstoMet |
70 | 56, 57, 58, 69 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
PsMet
pstoMet |
71 | 68, 70 | eqtrd 2656 |
. . . . . . . . . . . . . 14
PsMet
pstoMet |
72 | 67, 63 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
PsMet
pstoMet pstoMet |
73 | 7 | pstmfval 29939 |
. . . . . . . . . . . . . . . 16
PsMet
pstoMet |
74 | 56, 57, 59, 73 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
PsMet
pstoMet |
75 | 72, 74 | eqtrd 2656 |
. . . . . . . . . . . . . 14
PsMet
pstoMet |
76 | 71, 75 | oveq12d 6668 |
. . . . . . . . . . . . 13
PsMet
pstoMetpstoMet |
77 | 61, 66, 76 | 3brtr4d 4685 |
. . . . . . . . . . . 12
PsMet
pstoMet pstoMetpstoMet |
78 | 77 | adantl6r 789 |
. . . . . . . . . . 11
PsMet
pstoMet pstoMetpstoMet |
79 | | elqsi 7800 |
. . . . . . . . . . . 12
|
80 | 79 | ad5antlr 771 |
. . . . . . . . . . 11
PsMet
|
81 | 78, 80 | r19.29a 3078 |
. . . . . . . . . 10
PsMet
pstoMet pstoMetpstoMet |
82 | 81 | adantl5r 788 |
. . . . . . . . 9
PsMet
pstoMet pstoMetpstoMet |
83 | 24 | ad4antlr 769 |
. . . . . . . . 9
PsMet
|
84 | 82, 83 | r19.29a 3078 |
. . . . . . . 8
PsMet
pstoMet pstoMetpstoMet |
85 | 84 | adantl4r 787 |
. . . . . . 7
PsMet pstoMet pstoMetpstoMet |
86 | 28 | ad3antlr 767 |
. . . . . . 7
PsMet
|
87 | 85, 86 | r19.29a 3078 |
. . . . . 6
PsMet
pstoMet
pstoMetpstoMet |
88 | 87 | ralrimiva 2966 |
. . . . 5
PsMet pstoMet pstoMetpstoMet |
89 | 88 | anasss 679 |
. . . 4
PsMet
pstoMet pstoMetpstoMet |
90 | 55, 89 | jca 554 |
. . 3
PsMet
pstoMet
pstoMet pstoMetpstoMet |
91 | 90 | ralrimivva 2971 |
. 2
PsMet
pstoMet pstoMet pstoMetpstoMet |
92 | | elfvex 6221 |
. . 3
PsMet
|
93 | | qsexg 7805 |
. . 3
|
94 | | isxmet 22129 |
. . 3
pstoMet pstoMet
pstoMet
pstoMet pstoMetpstoMet |
95 | 92, 93, 94 | 3syl 18 |
. 2
PsMet
pstoMet pstoMet
pstoMet
pstoMet pstoMetpstoMet |
96 | 33, 91, 95 | mpbir2and 957 |
1
PsMet
pstoMet |