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 eqtrid ⊢ ¬ 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 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 ∈ 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