Metamath Proof Explorer

Theorem mclsind

Description: Induction theorem for closure: any other set Q closed under the axioms and the hypotheses contains all the elements of the closure. (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
mclsax.a ⊢A=mAx⁡T
mclsax.l ⊢L=mSubst⁡T
mclsax.v ⊢V=mVR⁡T
mclsax.h ⊢H=mVH⁡T
mclsax.w ⊢W=mVars⁡T
mclsind.4 ⊢φ→B⊆Q
mclsind.5 ⊢φ∧v∈V→H⁡v∈Q
mclsind.6 ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈Q
Assertion mclsind ⊢φ→KCB⊆Q

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 mclsax.a ⊢A=mAx⁡T
8 mclsax.l ⊢L=mSubst⁡T
9 mclsax.v ⊢V=mVR⁡T
10 mclsax.h ⊢H=mVH⁡T
11 mclsax.w ⊢W=mVars⁡T
12 mclsind.4 ⊢φ→B⊆Q
13 mclsind.5 ⊢φ∧v∈V→H⁡v∈Q
14 mclsind.6 ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈Q
15 1 2 3 4 5 6 10 7 8 11 mclsval ⊢φ→KCB=⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
16 6 12 ssind ⊢φ→B⊆E∩Q
17 9 2 10 mvhf ⊢T∈mFS→H:V⟶E
18 4 17 syl ⊢φ→H:V⟶E
19 18 ffnd ⊢φ→HFnV
20 18 ffvelcdmda ⊢φ∧v∈V→H⁡v∈E
21 20 13 elind ⊢φ∧v∈V→H⁡v∈E∩Q
22 21 ralrimiva ⊢φ→∀v∈VH⁡v∈E∩Q
23 ffnfv ⊢H:V⟶E∩Q↔HFnV∧∀v∈VH⁡v∈E∩Q
24 19 22 23 sylanbrc ⊢φ→H:V⟶E∩Q
25 24 frnd ⊢φ→ran⁡H⊆E∩Q
26 16 25 unssd ⊢φ→B∪ran⁡H⊆E∩Q
27 id ⊢so∪ran⁡H⊆E∩Q→so∪ran⁡H⊆E∩Q
28 inss2 ⊢E∩Q⊆Q
29 27 28 sstrdi ⊢so∪ran⁡H⊆E∩Q→so∪ran⁡H⊆Q
30 4 adantr ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→T∈mFS
31 eqid ⊢mREx⁡T=mREx⁡T
32 9 31 8 2 msubff ⊢T∈mFS→L:mREx⁡T↑𝑝𝑚V⟶EE
33 frn ⊢L:mREx⁡T↑𝑝𝑚V⟶EE→ran⁡L⊆EE
34 30 32 33 3syl ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→ran⁡L⊆EE
35 simpr2 ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→s∈ran⁡L
36 34 35 sseldd ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→s∈EE
37 elmapi ⊢s∈EE→s:E⟶E
38 36 37 syl ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→s:E⟶E
39 eqid ⊢mStat⁡T=mStat⁡T
40 7 39 maxsta ⊢T∈mFS→A⊆mStat⁡T
41 30 40 syl ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→A⊆mStat⁡T
42 eqid ⊢mPreSt⁡T=mPreSt⁡T
43 42 39 mstapst ⊢mStat⁡T⊆mPreSt⁡T
44 41 43 sstrdi ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→A⊆mPreSt⁡T
45 simpr1 ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→mop∈A
46 44 45 sseldd ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→mop∈mPreSt⁡T
47 1 2 42 elmpst ⊢mop∈mPreSt⁡T↔m⊆D∧m-1=m∧o⊆E∧o∈Fin∧p∈E
48 47 simp3bi ⊢mop∈mPreSt⁡T→p∈E
49 46 48 syl ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→p∈E
50 38 49 ffvelcdmd ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→s⁡p∈E
51 50 3adant3 ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E
52 51 14 elind ⊢φ∧mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
53 52 3exp ⊢φ→mop∈A∧s∈ran⁡L∧so∪ran⁡H⊆Q→∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
54 53 3expd ⊢φ→mop∈A→s∈ran⁡L→so∪ran⁡H⊆Q→∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
55 54 imp31 ⊢φ∧mop∈A∧s∈ran⁡L→so∪ran⁡H⊆Q→∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
56 29 55 syl5 ⊢φ∧mop∈A∧s∈ran⁡L→so∪ran⁡H⊆E∩Q→∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
57 56 impd ⊢φ∧mop∈A∧s∈ran⁡L→so∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
58 57 ralrimiva ⊢φ∧mop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
59 58 ex ⊢φ→mop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
60 59 alrimiv ⊢φ→∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
61 60 alrimivv ⊢φ→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
62 2 fvexi ⊢E∈V
63 62 inex1 ⊢E∩Q∈V
64 sseq2 ⊢c=E∩Q→B∪ran⁡H⊆c↔B∪ran⁡H⊆E∩Q
65 sseq2 ⊢c=E∩Q→so∪ran⁡H⊆c↔so∪ran⁡H⊆E∩Q
66 65 anbi1d ⊢c=E∩Q→so∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔so∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K
67 eleq2 ⊢c=E∩Q→s⁡p∈c↔s⁡p∈E∩Q
68 66 67 imbi12d ⊢c=E∩Q→so∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔so∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
69 68 ralbidv ⊢c=E∩Q→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
70 69 imbi2d ⊢c=E∩Q→mop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔mop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
71 70 albidv ⊢c=E∩Q→∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
72 71 2albidv ⊢c=E∩Q→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
73 64 72 anbi12d ⊢c=E∩Q→B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔B∪ran⁡H⊆E∩Q∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
74 63 73 elab ⊢E∩Q∈c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔B∪ran⁡H⊆E∩Q∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆E∩Q∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈E∩Q
75 26 61 74 sylanbrc ⊢φ→E∩Q∈c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
76 intss1 ⊢E∩Q∈c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c⊆E∩Q
77 75 76 syl ⊢φ→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c⊆E∩Q
78 77 28 sstrdi ⊢φ→⋂c|B∪ran⁡H⊆c∧∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c⊆Q
79 15 78 eqsstrd ⊢φ→KCB⊆Q