Metamath Proof Explorer

Theorem mclsssvlem

Description: Lemma for mclsssv . (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
mclsval.h ⊢H=mVH⁡T
mclsval.a ⊢A=mAx⁡T
mclsval.s ⊢S=mSubst⁡T
mclsval.v ⊢V=mVars⁡T
Assertion mclsssvlem ⊢φ→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c⊆E

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 mclsval.h ⊢H=mVH⁡T
8 mclsval.a ⊢A=mAx⁡T
9 mclsval.s ⊢S=mSubst⁡T
10 mclsval.v ⊢V=mVars⁡T
11 eqid ⊢mVR⁡T=mVR⁡T
12 11 2 7 mvhf ⊢T∈mFS→H:mVR⁡T⟶E
13 4 12 syl ⊢φ→H:mVR⁡T⟶E
14 13 frnd ⊢φ→ran⁡H⊆E
15 6 14 unssd ⊢φ→B∪ran⁡H⊆E
16 9 2 msubf ⊢s∈ran⁡S→s:E⟶E
17 eqid ⊢mStat⁡T=mStat⁡T
18 8 17 maxsta ⊢T∈mFS→A⊆mStat⁡T
19 4 18 syl ⊢φ→A⊆mStat⁡T
20 eqid ⊢mPreSt⁡T=mPreSt⁡T
21 20 17 mstapst ⊢mStat⁡T⊆mPreSt⁡T
22 19 21 sstrdi ⊢φ→A⊆mPreSt⁡T
23 22 sselda ⊢φ∧mop∈A→mop∈mPreSt⁡T
24 1 2 20 elmpst ⊢mop∈mPreSt⁡T↔m⊆D∧m-1=m∧o⊆E∧o∈Fin∧p∈E
25 24 simp3bi ⊢mop∈mPreSt⁡T→p∈E
26 23 25 syl ⊢φ∧mop∈A→p∈E
27 ffvelcdm ⊢s:E⟶E∧p∈E→s⁡p∈E
28 16 26 27 syl2anr ⊢φ∧mop∈A∧s∈ran⁡S→s⁡p∈E
29 28 a1d ⊢φ∧mop∈A∧s∈ran⁡S→so∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
30 29 ralrimiva ⊢φ∧mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
31 30 ex ⊢φ→mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
32 31 alrimiv ⊢φ→∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
33 32 alrimivv ⊢φ→∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
34 2 fvexi ⊢E∈V
35 sseq2 ⊢c=E→B∪ran⁡H⊆c↔B∪ran⁡H⊆E
36 sseq2 ⊢c=E→so∪ran⁡H⊆c↔so∪ran⁡H⊆E
37 36 anbi1d ⊢c=E→so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K↔so∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K
38 eleq2 ⊢c=E→s⁡p∈c↔s⁡p∈E
39 37 38 imbi12d ⊢c=E→so∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔so∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
40 39 ralbidv ⊢c=E→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
41 40 imbi2d ⊢c=E→mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔mop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
42 41 albidv ⊢c=E→∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
43 42 2albidv ⊢c=E→∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
44 35 43 anbi12d ⊢c=E→B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔B∪ran⁡H⊆E∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
45 34 44 elab ⊢E∈c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c↔B∪ran⁡H⊆E∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆E∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈E
46 15 33 45 sylanbrc ⊢φ→E∈c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c
47 intss1 ⊢E∈c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c⊆E
48 46 47 syl ⊢φ→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Sso∪ran⁡H⊆c∧∀x∀yxmy→V⁡s⁡H⁡x×V⁡s⁡H⁡y⊆K→s⁡p∈c⊆E