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