Metamath Proof Explorer


Theorem mclsssv

Description: The closure of a set of expressions is a set of expressions. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d 𝐷 = ( mDV ‘ 𝑇 )
mclsval.e 𝐸 = ( mEx ‘ 𝑇 )
mclsval.c 𝐶 = ( mCls ‘ 𝑇 )
mclsval.1 ( 𝜑𝑇 ∈ mFS )
mclsval.2 ( 𝜑𝐾𝐷 )
mclsval.3 ( 𝜑𝐵𝐸 )
Assertion mclsssv ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝐸 )

Proof

Step Hyp Ref Expression
1 mclsval.d 𝐷 = ( mDV ‘ 𝑇 )
2 mclsval.e 𝐸 = ( mEx ‘ 𝑇 )
3 mclsval.c 𝐶 = ( mCls ‘ 𝑇 )
4 mclsval.1 ( 𝜑𝑇 ∈ mFS )
5 mclsval.2 ( 𝜑𝐾𝐷 )
6 mclsval.3 ( 𝜑𝐵𝐸 )
7 eqid ( mVH ‘ 𝑇 ) = ( mVH ‘ 𝑇 )
8 eqid ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
9 eqid ( mSubst ‘ 𝑇 ) = ( mSubst ‘ 𝑇 )
10 eqid ( mVars ‘ 𝑇 ) = ( mVars ‘ 𝑇 )
11 1 2 3 4 5 6 7 8 9 10 mclsval ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚𝑜𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠𝑝 ) ∈ 𝑐 ) ) ) } )
12 1 2 3 4 5 6 7 8 9 10 mclsssvlem ( 𝜑 { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚𝑜𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 )
13 11 12 eqsstrd ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝐸 )