Step | Hyp | Ref
| Expression |
1 | | pstmval.1 |
. . . . 5
~Met |
2 | 1 | pstmval 29938 |
. . . 4
PsMet
pstoMet
|
3 | 2 | 3ad2ant1 1082 |
. . 3
PsMet
pstoMet
|
4 | 3 | oveqd 6667 |
. 2
PsMet
pstoMet
|
5 | | fvex 6201 |
. . . . . 6
~Met |
6 | 1, 5 | eqeltri 2697 |
. . . . 5
|
7 | 6 | ecelqsi 7803 |
. . . 4
|
8 | 7 | 3ad2ant2 1083 |
. . 3
PsMet
|
9 | 6 | ecelqsi 7803 |
. . . 4
|
10 | 9 | 3ad2ant3 1084 |
. . 3
PsMet
|
11 | | rexeq 3139 |
. . . . . 6
|
12 | 11 | abbidv 2741 |
. . . . 5
|
13 | 12 | unieqd 4446 |
. . . 4
|
14 | | rexeq 3139 |
. . . . . . 7
|
15 | 14 | rexbidv 3052 |
. . . . . 6
|
16 | 15 | abbidv 2741 |
. . . . 5
|
17 | 16 | unieqd 4446 |
. . . 4
|
18 | | eqid 2622 |
. . . 4
|
19 | | ecexg 7746 |
. . . . . . 7
|
20 | 6, 19 | ax-mp 5 |
. . . . . 6
|
21 | | ecexg 7746 |
. . . . . . 7
|
22 | 6, 21 | ax-mp 5 |
. . . . . 6
|
23 | 20, 22 | ab2rexex 7159 |
. . . . 5
|
24 | 23 | uniex 6953 |
. . . 4
|
25 | 13, 17, 18, 24 | ovmpt2 6796 |
. . 3
|
26 | 8, 10, 25 | syl2anc 693 |
. 2
PsMet
|
27 | | simpr3 1069 |
. . . . . . . . . . 11
PsMet
|
28 | | simpl1 1064 |
. . . . . . . . . . . 12
PsMet
PsMet |
29 | | simpr1 1067 |
. . . . . . . . . . . . . 14
PsMet
|
30 | | metidss 29934 |
. . . . . . . . . . . . . . . . . . . 20
PsMet
~Met
|
31 | 1, 30 | syl5eqss 3649 |
. . . . . . . . . . . . . . . . . . 19
PsMet
|
32 | | xpss 5226 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 31, 32 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
PsMet
|
34 | | df-rel 5121 |
. . . . . . . . . . . . . . . . . 18
|
35 | 33, 34 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
PsMet
|
36 | 35 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
PsMet
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . 15
PsMet
|
38 | | relelec 7787 |
. . . . . . . . . . . . . . 15
|
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . 14
PsMet
|
40 | 29, 39 | mpbid 222 |
. . . . . . . . . . . . 13
PsMet
|
41 | 1 | breqi 4659 |
. . . . . . . . . . . . 13
~Met |
42 | 40, 41 | sylib 208 |
. . . . . . . . . . . 12
PsMet
~Met |
43 | | simpr2 1068 |
. . . . . . . . . . . . . 14
PsMet
|
44 | | relelec 7787 |
. . . . . . . . . . . . . . 15
|
45 | 37, 44 | syl 17 |
. . . . . . . . . . . . . 14
PsMet
|
46 | 43, 45 | mpbid 222 |
. . . . . . . . . . . . 13
PsMet
|
47 | 1 | breqi 4659 |
. . . . . . . . . . . . 13
~Met |
48 | 46, 47 | sylib 208 |
. . . . . . . . . . . 12
PsMet
~Met |
49 | | metideq 29936 |
. . . . . . . . . . . 12
PsMet ~Met
~Met
|
50 | 28, 42, 48, 49 | syl12anc 1324 |
. . . . . . . . . . 11
PsMet
|
51 | 27, 50 | eqtr4d 2659 |
. . . . . . . . . 10
PsMet
|
52 | 51 | adantlr 751 |
. . . . . . . . 9
PsMet
|
53 | 52 | 3anassrs 1290 |
. . . . . . . 8
PsMet
|
54 | | oveq1 6657 |
. . . . . . . . . . . 12
|
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . 11
|
56 | | oveq2 6658 |
. . . . . . . . . . . 12
|
57 | 56 | eqeq2d 2632 |
. . . . . . . . . . 11
|
58 | 55, 57 | cbvrex2v 3180 |
. . . . . . . . . 10
|
59 | 58 | biimpi 206 |
. . . . . . . . 9
|
60 | 59 | adantl 482 |
. . . . . . . 8
PsMet
|
61 | 53, 60 | r19.29vva 3081 |
. . . . . . 7
PsMet
|
62 | | simpl1 1064 |
. . . . . . . . . 10
PsMet
PsMet |
63 | | simpl2 1065 |
. . . . . . . . . 10
PsMet
|
64 | | psmet0 22113 |
. . . . . . . . . 10
PsMet |
65 | 62, 63, 64 | syl2anc 693 |
. . . . . . . . 9
PsMet
|
66 | | relelec 7787 |
. . . . . . . . . . 11
|
67 | 62, 35, 66 | 3syl 18 |
. . . . . . . . . 10
PsMet
|
68 | 1 | a1i 11 |
. . . . . . . . . . 11
PsMet
~Met |
69 | 68 | breqd 4664 |
. . . . . . . . . 10
PsMet
~Met |
70 | | metidv 29935 |
. . . . . . . . . . 11
PsMet
~Met |
71 | 62, 63, 63, 70 | syl12anc 1324 |
. . . . . . . . . 10
PsMet
~Met
|
72 | 67, 69, 71 | 3bitrd 294 |
. . . . . . . . 9
PsMet
|
73 | 65, 72 | mpbird 247 |
. . . . . . . 8
PsMet
|
74 | | simpl3 1066 |
. . . . . . . . . 10
PsMet
|
75 | | psmet0 22113 |
. . . . . . . . . 10
PsMet |
76 | 62, 74, 75 | syl2anc 693 |
. . . . . . . . 9
PsMet
|
77 | | relelec 7787 |
. . . . . . . . . . 11
|
78 | 62, 35, 77 | 3syl 18 |
. . . . . . . . . 10
PsMet
|
79 | 68 | breqd 4664 |
. . . . . . . . . 10
PsMet
~Met |
80 | | metidv 29935 |
. . . . . . . . . . 11
PsMet
~Met |
81 | 62, 74, 74, 80 | syl12anc 1324 |
. . . . . . . . . 10
PsMet
~Met
|
82 | 78, 79, 81 | 3bitrd 294 |
. . . . . . . . 9
PsMet
|
83 | 76, 82 | mpbird 247 |
. . . . . . . 8
PsMet
|
84 | | simpr 477 |
. . . . . . . 8
PsMet
|
85 | | rspceov 6692 |
. . . . . . . 8
|
86 | 73, 83, 84, 85 | syl3anc 1326 |
. . . . . . 7
PsMet
|
87 | 61, 86 | impbida 877 |
. . . . . 6
PsMet
|
88 | 87 | abbidv 2741 |
. . . . 5
PsMet
|
89 | | df-sn 4178 |
. . . . 5
|
90 | 88, 89 | syl6eqr 2674 |
. . . 4
PsMet
|
91 | 90 | unieqd 4446 |
. . 3
PsMet
|
92 | | ovex 6678 |
. . . 4
|
93 | 92 | unisn 4451 |
. . 3
|
94 | 91, 93 | syl6eq 2672 |
. 2
PsMet
|
95 | 4, 26, 94 | 3eqtrd 2660 |
1
PsMet
pstoMet |