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 syl5eq
 |-  ( -. 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 syl5bb
 |-  ( 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 syl5bb
 |-  ( 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 ) )