Metamath Proof Explorer

Theorem ssmclslem

Description: Lemma for ssmcls . (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
mclsval.1 ⊢φ→T∈mFS
mclsval.2 ⊢φ→K⊆D
mclsval.3 ⊢φ→B⊆E
ssmclslem.h ⊢H=mVH⁡T
Assertion ssmclslem ⊢φ→B∪ran⁡H⊆KCB

Proof

Step Hyp Ref Expression
1 mclsval.d ⊢D=mDV⁡T
2 mclsval.e ⊢E=mEx⁡T
3 mclsval.c ⊢C=mCls⁡T
4 mclsval.1 ⊢φ→T∈mFS
5 mclsval.2 ⊢φ→K⊆D
6 mclsval.3 ⊢φ→B⊆E
7 ssmclslem.h ⊢H=mVH⁡T
8 simpl ⊢B∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c→B∪ran⁡H⊆c
9 8 a1i ⊢φ→B∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c→B∪ran⁡H⊆c
10 9 alrimiv ⊢φ→∀cB∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c→B∪ran⁡H⊆c
11 ssintab ⊢B∪ran⁡H⊆⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c↔∀cB∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c→B∪ran⁡H⊆c
12 10 11 sylibr ⊢φ→B∪ran⁡H⊆⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c
13 eqid ⊢mAx⁡T=mAx⁡T
14 eqid ⊢mSubst⁡T=mSubst⁡T
15 eqid ⊢mVars⁡T=mVars⁡T
16 1 2 3 4 5 6 7 13 14 15 mclsval ⊢φ→KCB=⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡H⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡H⁡x×mVars⁡T⁡s⁡H⁡y⊆K→s⁡p∈c
17 12 16 sseqtrrd ⊢φ→B∪ran⁡H⊆KCB