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∈KCB→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∈KCB→¬KCB=∅
5 fvprc ⊢¬T∈V→mCls⁡T=∅
6 3 5 eqtrid ⊢¬T∈V→C=∅
7 6 oveqd ⊢¬T∈V→KCB=K∅B
8 0ov ⊢K∅B=∅
9 7 8 eqtrdi ⊢¬T∈V→KCB=∅
10 4 9 nsyl2 ⊢A∈KCB→T∈V
11 fveq2 ⊢t=T→mCls⁡t=mCls⁡T
12 11 3 eqtr4di ⊢t=T→mCls⁡t=C
13 12 oveqd ⊢t=T→KmCls⁡tB=KCB
14 13 eleq2d ⊢t=T→A∈KmCls⁡tB↔A∈KCB
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 bitrid ⊢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 bitrid ⊢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∈KmCls⁡tB→K∈𝒫mDV⁡t∧B∈𝒫mEx⁡t↔A∈KCB→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→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∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
36 35 elmpocl ⊢A∈KmCls⁡tB→K∈𝒫mDV⁡t∧B∈𝒫mEx⁡t
37 28 36 vtoclg ⊢T∈V→A∈KCB→K⊆D∧B⊆E
38 10 37 mpcom ⊢A∈KCB→K⊆D∧B⊆E
39 38 simpld ⊢A∈KCB→K⊆D
40 38 simprd ⊢A∈KCB→B⊆E
41 10 39 40 3jca ⊢A∈KCB→T∈V∧K⊆D∧B⊆E