Theorem mclsrcl

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

	Ref	Expression
Hypotheses	mclsval.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
	mclsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mclsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
Assertion	mclsrcl	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → ( 𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		mclsval.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
2		mclsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mclsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
4		n0i	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → ¬ ( 𝐾 𝐶 𝐵 ) = ∅ )
5		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mCls ‘ 𝑇 ) = ∅ )
6	3 5	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝐶 = ∅ )
7	6	oveqd	⊢ ( ¬ 𝑇 ∈ V → ( 𝐾 𝐶 𝐵 ) = ( 𝐾 ∅ 𝐵 ) )
8		0ov	⊢ ( 𝐾 ∅ 𝐵 ) = ∅
9	7 8	eqtrdi	⊢ ( ¬ 𝑇 ∈ V → ( 𝐾 𝐶 𝐵 ) = ∅ )
10	4 9	nsyl2	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → 𝑇 ∈ V )
11		fveq2	⊢ ( 𝑡 = 𝑇 → ( mCls ‘ 𝑡 ) = ( mCls ‘ 𝑇 ) )
12	11 3	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mCls ‘ 𝑡 ) = 𝐶 )
13	12	oveqd	⊢ ( 𝑡 = 𝑇 → ( 𝐾 ( mCls ‘ 𝑡 ) 𝐵 ) = ( 𝐾 𝐶 𝐵 ) )
14	13	eleq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐴 ∈ ( 𝐾 ( mCls ‘ 𝑡 ) 𝐵 ) ↔ 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) ) )
15		fvex	⊢ ( mDV ‘ 𝑡 ) ∈ V
16	15	elpw2	⊢ ( 𝐾 ∈ 𝒫 ( mDV ‘ 𝑡 ) ↔ 𝐾 ⊆ ( mDV ‘ 𝑡 ) )
17		fveq2	⊢ ( 𝑡 = 𝑇 → ( mDV ‘ 𝑡 ) = ( mDV ‘ 𝑇 ) )
18	17 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mDV ‘ 𝑡 ) = 𝐷 )
19	18	sseq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐾 ⊆ ( mDV ‘ 𝑡 ) ↔ 𝐾 ⊆ 𝐷 ) )
20	16 19	syl5bb	⊢ ( 𝑡 = 𝑇 → ( 𝐾 ∈ 𝒫 ( mDV ‘ 𝑡 ) ↔ 𝐾 ⊆ 𝐷 ) )
21		fvex	⊢ ( mEx ‘ 𝑡 ) ∈ V
22	21	elpw2	⊢ ( 𝐵 ∈ 𝒫 ( mEx ‘ 𝑡 ) ↔ 𝐵 ⊆ ( mEx ‘ 𝑡 ) )
23		fveq2	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = ( mEx ‘ 𝑇 ) )
24	23 2	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mEx ‘ 𝑡 ) = 𝐸 )
25	24	sseq2d	⊢ ( 𝑡 = 𝑇 → ( 𝐵 ⊆ ( mEx ‘ 𝑡 ) ↔ 𝐵 ⊆ 𝐸 ) )
26	22 25	syl5bb	⊢ ( 𝑡 = 𝑇 → ( 𝐵 ∈ 𝒫 ( mEx ‘ 𝑡 ) ↔ 𝐵 ⊆ 𝐸 ) )
27	20 26	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝐾 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∧ 𝐵 ∈ 𝒫 ( mEx ‘ 𝑡 ) ) ↔ ( 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸 ) ) )
28	14 27	imbi12d	⊢ ( 𝑡 = 𝑇 → ( ( 𝐴 ∈ ( 𝐾 ( mCls ‘ 𝑡 ) 𝐵 ) → ( 𝐾 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∧ 𝐵 ∈ 𝒫 ( mEx ‘ 𝑡 ) ) ) ↔ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → ( 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸 ) ) ) )
29		vex	⊢ 𝑡 ∈ V
30	15	pwex	⊢ 𝒫 ( mDV ‘ 𝑡 ) ∈ V
31	21	pwex	⊢ 𝒫 ( mEx ‘ 𝑡 ) ∈ V
32	30 31	mpoex	⊢ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) ∈ V
33		df-mcls	⊢ mCls = ( 𝑡 ∈ V ↦ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
34	33	fvmpt2	⊢ ( ( 𝑡 ∈ V ∧ ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) ∈ V ) → ( mCls ‘ 𝑡 ) = ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ) )
35	29 32 34	mp2an	⊢ ( mCls ‘ 𝑡 ) = ( 𝑑 ∈ 𝒫 ( mDV ‘ 𝑡 ) , ℎ ∈ 𝒫 ( mEx ‘ 𝑡 ) ↦ ∩ { 𝑐 ∣ ( ( ℎ ∪ ran ( mVH ‘ 𝑡 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑡 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑡 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑡 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑑 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
36	35	elmpocl	⊢ ( 𝐴 ∈ ( 𝐾 ( mCls ‘ 𝑡 ) 𝐵 ) → ( 𝐾 ∈ 𝒫 ( mDV ‘ 𝑡 ) ∧ 𝐵 ∈ 𝒫 ( mEx ‘ 𝑡 ) ) )
37	28 36	vtoclg	⊢ ( 𝑇 ∈ V → ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → ( 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸 ) ) )
38	10 37	mpcom	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → ( 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸 ) )
39	38	simpld	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → 𝐾 ⊆ 𝐷 )
40	38	simprd	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → 𝐵 ⊆ 𝐸 )
41	10 39 40	3jca	⊢ ( 𝐴 ∈ ( 𝐾 𝐶 𝐵 ) → ( 𝑇 ∈ V ∧ 𝐾 ⊆ 𝐷 ∧ 𝐵 ⊆ 𝐸 ) )