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 ⊆ K C B

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 ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → 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 ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ H ⁡ x × mVars ⁡ T ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → B ∪ ran ⁡ H ⊆ c
10 9 alrimiv ⊢ φ → ∀ c B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → 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 ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ H ⁡ x × mVars ⁡ T ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ ∀ c B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → 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 ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → 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 ⊢ φ → K C B = ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ T → ∀ s ∈ ran ⁡ mSubst ⁡ T s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ H ⁡ x × mVars ⁡ T ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
17 12 16 sseqtrrd ⊢ φ → B ∪ ran ⁡ H ⊆ K C B