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 K C B T V K D B 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 K C B ¬ K C B =
5 fvprc ¬ T V mCls T =
6 3 5 syl5eq ¬ T V C =
7 6 oveqd ¬ T V K C B = K B
8 0ov K B =
9 7 8 eqtrdi ¬ T V K C B =
10 4 9 nsyl2 A K C B T 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 K mCls t B A K C B
15 fvex mDV t V
16 15 elpw2 K 𝒫 mDV t K 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 mDV t K D
20 16 19 syl5bb t = T K 𝒫 mDV t K D
21 fvex mEx t V
22 21 elpw2 B 𝒫 mEx t B 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 mEx t B E
26 22 25 syl5bb t = T B 𝒫 mEx t B E
27 20 26 anbi12d t = T K 𝒫 mDV t B 𝒫 mEx t K D B E
28 14 27 imbi12d t = T A K mCls t B K 𝒫 mDV t B 𝒫 mEx t A K C B K D B E
29 vex t V
30 15 pwex 𝒫 mDV t V
31 21 pwex 𝒫 mEx t V
32 30 31 mpoex d 𝒫 mDV t , h 𝒫 mEx t c | h ran mVH t c m o p m o p mAx t s ran mSubst t s o ran mVH t c x y x m y mVars t s mVH t x × mVars t s mVH t y d s p c V
33 df-mcls mCls = t V d 𝒫 mDV t , h 𝒫 mEx t c | h ran mVH t c m o p m o p mAx t s ran mSubst t s o ran mVH t c x y x m y mVars t s mVH t x × mVars t s mVH t y d s p c
34 33 fvmpt2 t V d 𝒫 mDV t , h 𝒫 mEx t c | h ran mVH t c m o p m o p mAx t s ran mSubst t s o ran mVH t c x y x m y mVars t s mVH t x × mVars t s mVH t y d s p c V mCls t = d 𝒫 mDV t , h 𝒫 mEx t c | h ran mVH t c m o p m o p mAx t s ran mSubst t s o ran mVH t c x y x m y mVars t s mVH t x × mVars t s mVH t y d s p c
35 29 32 34 mp2an mCls t = d 𝒫 mDV t , h 𝒫 mEx t c | h ran mVH t c m o p m o p mAx t s ran mSubst t s o ran mVH t c x y x m y mVars t s mVH t x × mVars t s mVH t y d s p c
36 35 elmpocl A K mCls t B K 𝒫 mDV t B 𝒫 mEx t
37 28 36 vtoclg T V A K C B K D B E
38 10 37 mpcom A K C B K D B E
39 38 simpld A K C B K D
40 38 simprd A K C B B E
41 10 39 40 3jca A K C B T V K D B E