Metamath Proof Explorer

Theorem mclsrcl

Description: Reverse closure for the closure function. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d 
|- D = ( mDV ` T )
mclsval.e 
|- E = ( mEx ` T )
mclsval.c 
|- C = ( mCls ` T )
Assertion mclsrcl 
|- ( A e. ( K C B ) -> ( T e. _V /\ K C_ D /\ B C_ E ) )

Proof

Step Hyp Ref Expression
1 mclsval.d 
 |-  D = ( mDV ` T )
2 mclsval.e 
 |-  E = ( mEx ` T )
3 mclsval.c 
 |-  C = ( mCls ` T )
4 n0i 
 |-  ( A e. ( K C B ) -> -. ( K C B ) = (/) )
5 fvprc 
 |-  ( -. T e. _V -> ( mCls ` T ) = (/) )
6 3 5 eqtrid 
 |-  ( -. T e. _V -> C = (/) )
7 6 oveqd 
 |-  ( -. T e. _V -> ( K C B ) = ( K (/) B ) )
8 0ov 
 |-  ( K (/) B ) = (/)
9 7 8 eqtrdi 
 |-  ( -. T e. _V -> ( K C B ) = (/) )
10 4 9 nsyl2 
 |-  ( A e. ( K C B ) -> T e. _V )
11 fveq2 
 |-  ( t = T -> ( mCls ` t ) = ( mCls ` T ) )
12 11 3 eqtr4di 
 |-  ( t = T -> ( mCls ` t ) = C )
13 12 oveqd 
 |-  ( t = T -> ( K ( mCls ` t ) B ) = ( K C B ) )
14 13 eleq2d 
 |-  ( t = T -> ( A e. ( K ( mCls ` t ) B ) <-> A e. ( K C B ) ) )
15 fvex 
 |-  ( mDV ` t ) e. _V
16 15 elpw2 
 |-  ( K e. ~P ( mDV ` t ) <-> K C_ ( mDV ` t ) )
17 fveq2 
 |-  ( t = T -> ( mDV ` t ) = ( mDV ` T ) )
18 17 1 eqtr4di 
 |-  ( t = T -> ( mDV ` t ) = D )
19 18 sseq2d 
 |-  ( t = T -> ( K C_ ( mDV ` t ) <-> K C_ D ) )
20 16 19 bitrid 
 |-  ( t = T -> ( K e. ~P ( mDV ` t ) <-> K C_ D ) )
21 fvex 
 |-  ( mEx ` t ) e. _V
22 21 elpw2 
 |-  ( B e. ~P ( mEx ` t ) <-> B C_ ( mEx ` t ) )
23 fveq2 
 |-  ( t = T -> ( mEx ` t ) = ( mEx ` T ) )
24 23 2 eqtr4di 
 |-  ( t = T -> ( mEx ` t ) = E )
25 24 sseq2d 
 |-  ( t = T -> ( B C_ ( mEx ` t ) <-> B C_ E ) )
26 22 25 bitrid 
 |-  ( t = T -> ( B e. ~P ( mEx ` t ) <-> B C_ E ) )
27 20 26 anbi12d 
 |-  ( t = T -> ( ( K e. ~P ( mDV ` t ) /\ B e. ~P ( mEx ` t ) ) <-> ( K C_ D /\ B C_ E ) ) )
28 14 27 imbi12d 
 |-  ( t = T -> ( ( A e. ( K ( mCls ` t ) B ) -> ( K e. ~P ( mDV ` t ) /\ B e. ~P ( mEx ` t ) ) ) <-> ( A e. ( K C B ) -> ( K C_ D /\ B C_ E ) ) ) )
29 vex 
 |-  t e. _V
30 15 pwex 
 |-  ~P ( mDV ` t ) e. _V
31 21 pwex 
 |-  ~P ( mEx ` t ) e. _V
32 30 31 mpoex 
 |-  ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) e. _V
33 df-mcls 
 |-  mCls = ( t e. _V |-> ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) )
34 33 fvmpt2 
 |-  ( ( t e. _V /\ ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) e. _V ) -> ( mCls ` t ) = ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) )
35 29 32 34 mp2an 
 |-  ( mCls ` t ) = ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } )
36 35 elmpocl 
 |-  ( A e. ( K ( mCls ` t ) B ) -> ( K e. ~P ( mDV ` t ) /\ B e. ~P ( mEx ` t ) ) )
37 28 36 vtoclg 
 |-  ( T e. _V -> ( A e. ( K C B ) -> ( K C_ D /\ B C_ E ) ) )
38 10 37 mpcom 
 |-  ( A e. ( K C B ) -> ( K C_ D /\ B C_ E ) )
39 38 simpld 
 |-  ( A e. ( K C B ) -> K C_ D )
40 38 simprd 
 |-  ( A e. ( K C B ) -> B C_ E )
41 10 39 40 3jca 
 |-  ( A e. ( K C B ) -> ( T e. _V /\ K C_ D /\ B C_ E ) )