Metamath Proof Explorer


Theorem mthmpps

Description: Given a theorem, there is an explicitly definable witnessing provable pre-statement for the provability of the theorem. (However, this pre-statement requires infinitely many disjoint variable conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mthmpps.r R = mStRed T
mthmpps.j J = mPPSt T
mthmpps.u U = mThm T
mthmpps.d D = mDV T
mthmpps.v V = mVars T
mthmpps.z Z = V H A
mthmpps.m M = C D Z × Z
Assertion mthmpps T mFS C H A U M H A J R M H A = R C H A

Proof

Step Hyp Ref Expression
1 mthmpps.r R = mStRed T
2 mthmpps.j J = mPPSt T
3 mthmpps.u U = mThm T
4 mthmpps.d D = mDV T
5 mthmpps.v V = mVars T
6 mthmpps.z Z = V H A
7 mthmpps.m M = C D Z × Z
8 eqid mPreSt T = mPreSt T
9 3 8 mthmsta U mPreSt T
10 simpr T mFS C H A U C H A U
11 9 10 sselid T mFS C H A U C H A mPreSt T
12 eqid mEx T = mEx T
13 4 12 8 elmpst C H A mPreSt T C D C -1 = C H mEx T H Fin A mEx T
14 11 13 sylib T mFS C H A U C D C -1 = C H mEx T H Fin A mEx T
15 14 simp1d T mFS C H A U C D C -1 = C
16 15 simpld T mFS C H A U C D
17 difssd T mFS C H A U D Z × Z D
18 16 17 unssd T mFS C H A U C D Z × Z D
19 7 18 eqsstrid T mFS C H A U M D
20 15 simprd T mFS C H A U C -1 = C
21 cnvdif D Z × Z -1 = D -1 Z × Z -1
22 cnvdif mVR T × mVR T I -1 = mVR T × mVR T -1 I -1
23 cnvxp mVR T × mVR T -1 = mVR T × mVR T
24 cnvi I -1 = I
25 23 24 difeq12i mVR T × mVR T -1 I -1 = mVR T × mVR T I
26 22 25 eqtri mVR T × mVR T I -1 = mVR T × mVR T I
27 eqid mVR T = mVR T
28 27 4 mdvval D = mVR T × mVR T I
29 28 cnveqi D -1 = mVR T × mVR T I -1
30 26 29 28 3eqtr4i D -1 = D
31 cnvxp Z × Z -1 = Z × Z
32 30 31 difeq12i D -1 Z × Z -1 = D Z × Z
33 21 32 eqtri D Z × Z -1 = D Z × Z
34 33 a1i T mFS C H A U D Z × Z -1 = D Z × Z
35 20 34 uneq12d T mFS C H A U C -1 D Z × Z -1 = C D Z × Z
36 7 cnveqi M -1 = C D Z × Z -1
37 cnvun C D Z × Z -1 = C -1 D Z × Z -1
38 36 37 eqtri M -1 = C -1 D Z × Z -1
39 35 38 7 3eqtr4g T mFS C H A U M -1 = M
40 19 39 jca T mFS C H A U M D M -1 = M
41 14 simp2d T mFS C H A U H mEx T H Fin
42 14 simp3d T mFS C H A U A mEx T
43 4 12 8 elmpst M H A mPreSt T M D M -1 = M H mEx T H Fin A mEx T
44 40 41 42 43 syl3anbrc T mFS C H A U M H A mPreSt T
45 1 2 3 elmthm C H A U x J R x = R C H A
46 10 45 sylib T mFS C H A U x J R x = R C H A
47 eqid mCls T = mCls T
48 simpll T mFS C H A U x J R x = R C H A T mFS
49 19 adantr T mFS C H A U x J R x = R C H A M D
50 41 simpld T mFS C H A U H mEx T
51 50 adantr T mFS C H A U x J R x = R C H A H mEx T
52 8 2 mppspst J mPreSt T
53 simprl T mFS C H A U x J R x = R C H A x J
54 52 53 sselid T mFS C H A U x J R x = R C H A x mPreSt T
55 8 mpst123 x mPreSt T x = 1 st 1 st x 2 nd 1 st x 2 nd x
56 54 55 syl T mFS C H A U x J R x = R C H A x = 1 st 1 st x 2 nd 1 st x 2 nd x
57 56 fveq2d T mFS C H A U x J R x = R C H A R x = R 1 st 1 st x 2 nd 1 st x 2 nd x
58 simprr T mFS C H A U x J R x = R C H A R x = R C H A
59 57 58 eqtr3d T mFS C H A U x J R x = R C H A R 1 st 1 st x 2 nd 1 st x 2 nd x = R C H A
60 56 54 eqeltrrd T mFS C H A U x J R x = R C H A 1 st 1 st x 2 nd 1 st x 2 nd x mPreSt T
61 eqid V 2 nd 1 st x 2 nd x = V 2 nd 1 st x 2 nd x
62 5 8 1 61 msrval 1 st 1 st x 2 nd 1 st x 2 nd x mPreSt T R 1 st 1 st x 2 nd 1 st x 2 nd x = 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x 2 nd 1 st x 2 nd x
63 60 62 syl T mFS C H A U x J R x = R C H A R 1 st 1 st x 2 nd 1 st x 2 nd x = 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x 2 nd 1 st x 2 nd x
64 5 8 1 6 msrval C H A mPreSt T R C H A = C Z × Z H A
65 11 64 syl T mFS C H A U R C H A = C Z × Z H A
66 65 adantr T mFS C H A U x J R x = R C H A R C H A = C Z × Z H A
67 59 63 66 3eqtr3d T mFS C H A U x J R x = R C H A 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x 2 nd 1 st x 2 nd x = C Z × Z H A
68 fvex 1 st 1 st x V
69 68 inex1 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x V
70 fvex 2 nd 1 st x V
71 fvex 2 nd x V
72 69 70 71 otth 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x 2 nd 1 st x 2 nd x = C Z × Z H A 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x = C Z × Z 2 nd 1 st x = H 2 nd x = A
73 67 72 sylib T mFS C H A U x J R x = R C H A 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x = C Z × Z 2 nd 1 st x = H 2 nd x = A
74 73 simp1d T mFS C H A U x J R x = R C H A 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x = C Z × Z
75 73 simp2d T mFS C H A U x J R x = R C H A 2 nd 1 st x = H
76 73 simp3d T mFS C H A U x J R x = R C H A 2 nd x = A
77 76 sneqd T mFS C H A U x J R x = R C H A 2 nd x = A
78 75 77 uneq12d T mFS C H A U x J R x = R C H A 2 nd 1 st x 2 nd x = H A
79 78 imaeq2d T mFS C H A U x J R x = R C H A V 2 nd 1 st x 2 nd x = V H A
80 79 unieqd T mFS C H A U x J R x = R C H A V 2 nd 1 st x 2 nd x = V H A
81 80 6 eqtr4di T mFS C H A U x J R x = R C H A V 2 nd 1 st x 2 nd x = Z
82 81 sqxpeqd T mFS C H A U x J R x = R C H A V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x = Z × Z
83 82 ineq2d T mFS C H A U x J R x = R C H A 1 st 1 st x V 2 nd 1 st x 2 nd x × V 2 nd 1 st x 2 nd x = 1 st 1 st x Z × Z
84 74 83 eqtr3d T mFS C H A U x J R x = R C H A C Z × Z = 1 st 1 st x Z × Z
85 inss1 C Z × Z C
86 84 85 eqsstrrdi T mFS C H A U x J R x = R C H A 1 st 1 st x Z × Z C
87 eqidd T mFS C H A U x J R x = R C H A 1 st 1 st x = 1 st 1 st x
88 87 75 76 oteq123d T mFS C H A U x J R x = R C H A 1 st 1 st x 2 nd 1 st x 2 nd x = 1 st 1 st x H A
89 56 88 eqtrd T mFS C H A U x J R x = R C H A x = 1 st 1 st x H A
90 89 54 eqeltrrd T mFS C H A U x J R x = R C H A 1 st 1 st x H A mPreSt T
91 4 12 8 elmpst 1 st 1 st x H A mPreSt T 1 st 1 st x D 1 st 1 st x -1 = 1 st 1 st x H mEx T H Fin A mEx T
92 91 simp1bi 1 st 1 st x H A mPreSt T 1 st 1 st x D 1 st 1 st x -1 = 1 st 1 st x
93 92 simpld 1 st 1 st x H A mPreSt T 1 st 1 st x D
94 90 93 syl T mFS C H A U x J R x = R C H A 1 st 1 st x D
95 94 ssdifd T mFS C H A U x J R x = R C H A 1 st 1 st x Z × Z D Z × Z
96 unss12 1 st 1 st x Z × Z C 1 st 1 st x Z × Z D Z × Z 1 st 1 st x Z × Z 1 st 1 st x Z × Z C D Z × Z
97 86 95 96 syl2anc T mFS C H A U x J R x = R C H A 1 st 1 st x Z × Z 1 st 1 st x Z × Z C D Z × Z
98 inundif 1 st 1 st x Z × Z 1 st 1 st x Z × Z = 1 st 1 st x
99 98 eqcomi 1 st 1 st x = 1 st 1 st x Z × Z 1 st 1 st x Z × Z
100 97 99 7 3sstr4g T mFS C H A U x J R x = R C H A 1 st 1 st x M
101 ssidd T mFS C H A U x J R x = R C H A H H
102 4 12 47 48 49 51 100 101 ss2mcls T mFS C H A U x J R x = R C H A 1 st 1 st x mCls T H M mCls T H
103 89 53 eqeltrrd T mFS C H A U x J R x = R C H A 1 st 1 st x H A J
104 8 2 47 elmpps 1 st 1 st x H A J 1 st 1 st x H A mPreSt T A 1 st 1 st x mCls T H
105 104 simprbi 1 st 1 st x H A J A 1 st 1 st x mCls T H
106 103 105 syl T mFS C H A U x J R x = R C H A A 1 st 1 st x mCls T H
107 102 106 sseldd T mFS C H A U x J R x = R C H A A M mCls T H
108 46 107 rexlimddv T mFS C H A U A M mCls T H
109 8 2 47 elmpps M H A J M H A mPreSt T A M mCls T H
110 44 108 109 sylanbrc T mFS C H A U M H A J
111 7 ineq1i M Z × Z = C D Z × Z Z × Z
112 indir C D Z × Z Z × Z = C Z × Z D Z × Z Z × Z
113 disjdifr D Z × Z Z × Z =
114 0ss C Z × Z
115 113 114 eqsstri D Z × Z Z × Z C Z × Z
116 ssequn2 D Z × Z Z × Z C Z × Z C Z × Z D Z × Z Z × Z = C Z × Z
117 115 116 mpbi C Z × Z D Z × Z Z × Z = C Z × Z
118 111 112 117 3eqtri M Z × Z = C Z × Z
119 118 a1i T mFS C H A U M Z × Z = C Z × Z
120 119 oteq1d T mFS C H A U M Z × Z H A = C Z × Z H A
121 5 8 1 6 msrval M H A mPreSt T R M H A = M Z × Z H A
122 44 121 syl T mFS C H A U R M H A = M Z × Z H A
123 120 122 65 3eqtr4d T mFS C H A U R M H A = R C H A
124 110 123 jca T mFS C H A U M H A J R M H A = R C H A
125 124 ex T mFS C H A U M H A J R M H A = R C H A
126 1 2 3 mthmi M H A J R M H A = R C H A C H A U
127 125 126 impbid1 T mFS C H A U M H A J R M H A = R C H A