Step | Hyp | Ref
| Expression |
1 | | mthmpps.m |
. . . . . . . 8
|
2 | | mthmpps.u |
. . . . . . . . . . . . . 14
mThm |
3 | | eqid 2622 |
. . . . . . . . . . . . . 14
mPreSt mPreSt |
4 | 2, 3 | mthmsta 31475 |
. . . . . . . . . . . . 13
mPreSt |
5 | | simpr 477 |
. . . . . . . . . . . . 13
mFS |
6 | 4, 5 | sseldi 3601 |
. . . . . . . . . . . 12
mFS mPreSt |
7 | | mthmpps.d |
. . . . . . . . . . . . 13
mDV |
8 | | eqid 2622 |
. . . . . . . . . . . . 13
mEx mEx |
9 | 7, 8, 3 | elmpst 31433 |
. . . . . . . . . . . 12
mPreSt
mEx mEx |
10 | 6, 9 | sylib 208 |
. . . . . . . . . . 11
mFS mEx
mEx |
11 | 10 | simp1d 1073 |
. . . . . . . . . 10
mFS
|
12 | 11 | simpld 475 |
. . . . . . . . 9
mFS |
13 | | difssd 3738 |
. . . . . . . . 9
mFS |
14 | 12, 13 | unssd 3789 |
. . . . . . . 8
mFS |
15 | 1, 14 | syl5eqss 3649 |
. . . . . . 7
mFS |
16 | 11 | simprd 479 |
. . . . . . . . 9
mFS
|
17 | | cnvdif 5539 |
. . . . . . . . . . 11
|
18 | | cnvdif 5539 |
. . . . . . . . . . . . . 14
mVR mVR
mVR mVR |
19 | | cnvxp 5551 |
. . . . . . . . . . . . . . 15
mVR mVR mVR mVR |
20 | | cnvi 5537 |
. . . . . . . . . . . . . . 15
|
21 | 19, 20 | difeq12i 3726 |
. . . . . . . . . . . . . 14
mVR mVR mVR mVR |
22 | 18, 21 | eqtri 2644 |
. . . . . . . . . . . . 13
mVR mVR
mVR mVR |
23 | | eqid 2622 |
. . . . . . . . . . . . . . 15
mVR mVR |
24 | 23, 7 | mdvval 31401 |
. . . . . . . . . . . . . 14
mVR mVR |
25 | 24 | cnveqi 5297 |
. . . . . . . . . . . . 13
mVR mVR
|
26 | 22, 25, 24 | 3eqtr4i 2654 |
. . . . . . . . . . . 12
|
27 | | cnvxp 5551 |
. . . . . . . . . . . 12
|
28 | 26, 27 | difeq12i 3726 |
. . . . . . . . . . 11
|
29 | 17, 28 | eqtri 2644 |
. . . . . . . . . 10
|
30 | 29 | a1i 11 |
. . . . . . . . 9
mFS |
31 | 16, 30 | uneq12d 3768 |
. . . . . . . 8
mFS |
32 | 1 | cnveqi 5297 |
. . . . . . . . 9
|
33 | | cnvun 5538 |
. . . . . . . . 9
|
34 | 32, 33 | eqtri 2644 |
. . . . . . . 8
|
35 | 31, 34, 1 | 3eqtr4g 2681 |
. . . . . . 7
mFS
|
36 | 15, 35 | jca 554 |
. . . . . 6
mFS
|
37 | 10 | simp2d 1074 |
. . . . . 6
mFS mEx |
38 | 10 | simp3d 1075 |
. . . . . 6
mFS
mEx |
39 | 7, 8, 3 | elmpst 31433 |
. . . . . 6
mPreSt
mEx mEx |
40 | 36, 37, 38, 39 | syl3anbrc 1246 |
. . . . 5
mFS mPreSt |
41 | | mthmpps.r |
. . . . . . . 8
mStRed |
42 | | mthmpps.j |
. . . . . . . 8
mPPSt |
43 | 41, 42, 2 | elmthm 31473 |
. . . . . . 7
|
44 | 5, 43 | sylib 208 |
. . . . . 6
mFS
|
45 | | eqid 2622 |
. . . . . . . 8
mCls mCls |
46 | | simpll 790 |
. . . . . . . 8
mFS
mFS |
47 | 15 | adantr 481 |
. . . . . . . 8
mFS
|
48 | 37 | simpld 475 |
. . . . . . . . 9
mFS mEx |
49 | 48 | adantr 481 |
. . . . . . . 8
mFS
mEx |
50 | 3, 42 | mppspst 31471 |
. . . . . . . . . . . . . . . . . . 19
mPreSt |
51 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
mFS
|
52 | 50, 51 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
mFS
mPreSt |
53 | 3 | mpst123 31437 |
. . . . . . . . . . . . . . . . . 18
mPreSt
|
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
mFS
|
55 | 54 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
mFS
|
56 | | simprr 796 |
. . . . . . . . . . . . . . . 16
mFS
|
57 | 55, 56 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
mFS
|
58 | 54, 52 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
mFS
mPreSt |
59 | | mthmpps.v |
. . . . . . . . . . . . . . . . 17
mVars |
60 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
61 | 59, 3, 41, 60 | msrval 31435 |
. . . . . . . . . . . . . . . 16
mPreSt |
62 | 58, 61 | syl 17 |
. . . . . . . . . . . . . . 15
mFS
|
63 | | mthmpps.z |
. . . . . . . . . . . . . . . . . 18
|
64 | 59, 3, 41, 63 | msrval 31435 |
. . . . . . . . . . . . . . . . 17
mPreSt
|
65 | 6, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
mFS |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . 15
mFS
|
67 | 57, 62, 66 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
mFS
|
68 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
69 | 68 | inex1 4799 |
. . . . . . . . . . . . . . 15
|
70 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
71 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
72 | 69, 70, 71 | otth 4953 |
. . . . . . . . . . . . . 14
|
73 | 67, 72 | sylib 208 |
. . . . . . . . . . . . 13
mFS
|
74 | 73 | simp1d 1073 |
. . . . . . . . . . . 12
mFS
|
75 | 73 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
mFS
|
76 | 73 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . 19
mFS
|
77 | 76 | sneqd 4189 |
. . . . . . . . . . . . . . . . . 18
mFS
|
78 | 75, 77 | uneq12d 3768 |
. . . . . . . . . . . . . . . . 17
mFS
|
79 | 78 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
mFS
|
80 | 79 | unieqd 4446 |
. . . . . . . . . . . . . . 15
mFS
|
81 | 80, 63 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
mFS
|
82 | 81 | sqxpeqd 5141 |
. . . . . . . . . . . . 13
mFS
|
83 | 82 | ineq2d 3814 |
. . . . . . . . . . . 12
mFS
|
84 | 74, 83 | eqtr3d 2658 |
. . . . . . . . . . 11
mFS
|
85 | | inss1 3833 |
. . . . . . . . . . 11
|
86 | 84, 85 | syl6eqssr 3656 |
. . . . . . . . . 10
mFS
|
87 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
mFS
|
88 | 87, 75, 76 | oteq123d 4417 |
. . . . . . . . . . . . . 14
mFS
|
89 | 54, 88 | eqtrd 2656 |
. . . . . . . . . . . . 13
mFS
|
90 | 89, 52 | eqeltrrd 2702 |
. . . . . . . . . . . 12
mFS
mPreSt |
91 | 7, 8, 3 | elmpst 31433 |
. . . . . . . . . . . . . 14
mPreSt mEx
mEx |
92 | 91 | simp1bi 1076 |
. . . . . . . . . . . . 13
mPreSt
|
93 | 92 | simpld 475 |
. . . . . . . . . . . 12
mPreSt
|
94 | 90, 93 | syl 17 |
. . . . . . . . . . 11
mFS
|
95 | 94 | ssdifd 3746 |
. . . . . . . . . 10
mFS
|
96 | | unss12 3785 |
. . . . . . . . . 10
|
97 | 86, 95, 96 | syl2anc 693 |
. . . . . . . . 9
mFS
|
98 | | inundif 4046 |
. . . . . . . . . 10
|
99 | 98 | eqcomi 2631 |
. . . . . . . . 9
|
100 | 97, 99, 1 | 3sstr4g 3646 |
. . . . . . . 8
mFS
|
101 | | ssid 3624 |
. . . . . . . . 9
|
102 | 101 | a1i 11 |
. . . . . . . 8
mFS
|
103 | 7, 8, 45, 46, 47, 49, 100, 102 | ss2mcls 31465 |
. . . . . . 7
mFS
mCls mCls |
104 | 89, 51 | eqeltrrd 2702 |
. . . . . . . 8
mFS
|
105 | 3, 42, 45 | elmpps 31470 |
. . . . . . . . 9
mPreSt
mCls |
106 | 105 | simprbi 480 |
. . . . . . . 8
mCls |
107 | 104, 106 | syl 17 |
. . . . . . 7
mFS
mCls |
108 | 103, 107 | sseldd 3604 |
. . . . . 6
mFS
mCls |
109 | 44, 108 | rexlimddv 3035 |
. . . . 5
mFS
mCls |
110 | 3, 42, 45 | elmpps 31470 |
. . . . 5
mPreSt
mCls |
111 | 40, 109, 110 | sylanbrc 698 |
. . . 4
mFS |
112 | 1 | ineq1i 3810 |
. . . . . . . 8
|
113 | | indir 3875 |
. . . . . . . 8
|
114 | | incom 3805 |
. . . . . . . . . . 11
|
115 | | disjdif 4040 |
. . . . . . . . . . 11
|
116 | 114, 115 | eqtri 2644 |
. . . . . . . . . 10
|
117 | | 0ss 3972 |
. . . . . . . . . 10
|
118 | 116, 117 | eqsstri 3635 |
. . . . . . . . 9
|
119 | | ssequn2 3786 |
. . . . . . . . 9
|
120 | 118, 119 | mpbi 220 |
. . . . . . . 8
|
121 | 112, 113,
120 | 3eqtri 2648 |
. . . . . . 7
|
122 | 121 | a1i 11 |
. . . . . 6
mFS
|
123 | 122 | oteq1d 4414 |
. . . . 5
mFS
|
124 | 59, 3, 41, 63 | msrval 31435 |
. . . . . 6
mPreSt
|
125 | 40, 124 | syl 17 |
. . . . 5
mFS |
126 | 123, 125,
65 | 3eqtr4d 2666 |
. . . 4
mFS |
127 | 111, 126 | jca 554 |
. . 3
mFS
|
128 | 127 | ex 450 |
. 2
mFS
|
129 | 41, 42, 2 | mthmi 31474 |
. 2
|
130 | 128, 129 | impbid1 215 |
1
mFS
|