Theorem ssmclslem

Description: Lemma for ssmcls . (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	⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
	ssmclslem.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
Assertion	ssmclslem	⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐾 𝐶 𝐵 ) )

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		ssmclslem.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
8		simpl	⊢ ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 )
9	8	a1i	⊢ ( 𝜑 → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ) )
10	9	alrimiv	⊢ ( 𝜑 → ∀ 𝑐 ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ) )
11		ssintab	⊢ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ↔ ∀ 𝑐 ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ) )
12	10 11	sylibr	⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
13		eqid	⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
14		eqid	⊢ ( mSubst ‘ 𝑇 ) = ( mSubst ‘ 𝑇 )
15		eqid	⊢ ( mVars ‘ 𝑇 ) = ( mVars ‘ 𝑇 )
16	1 2 3 4 5 6 7 13 14 15	mclsval	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
17	12 16	sseqtrrd	⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐾 𝐶 𝐵 ) )