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 sseldi
 |-  ( ( 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 sseldi
 |-  ( ( ( 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 >. ) ) ) )