Metamath Proof Explorer

Theorem mclsax

Description: The closure is closed under axiom application. (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
mclsax.4 ⊢φ→MOP∈A
mclsax.5 ⊢φ→S∈ran⁡L
mclsax.6 ⊢φ∧x∈O→S⁡x∈KCB
mclsax.7 ⊢φ∧v∈V→S⁡H⁡v∈KCB
mclsax.8 ⊢φ∧xMy∧a∈W⁡S⁡H⁡x∧b∈W⁡S⁡H⁡y→aKb
Assertion mclsax ⊢φ→S⁡P∈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 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 mclsax.4 ⊢φ→MOP∈A
13 mclsax.5 ⊢φ→S∈ran⁡L
14 mclsax.6 ⊢φ∧x∈O→S⁡x∈KCB
15 mclsax.7 ⊢φ∧v∈V→S⁡H⁡v∈KCB
16 mclsax.8 ⊢φ∧xMy∧a∈W⁡S⁡H⁡x∧b∈W⁡S⁡H⁡y→aKb
17 abid ⊢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↔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
18 intss1 ⊢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→⋂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
19 17 18 sylbir ⊢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⊆c
20 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
21 20 sseq1d ⊢φ→KCB⊆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⊆c
22 19 21 imbitrrid ⊢φ→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→KCB⊆c
23 sstr2 ⊢so∪ran⁡H⊆KCB→KCB⊆c→so∪ran⁡H⊆c
24 23 com12 ⊢KCB⊆c→so∪ran⁡H⊆KCB→so∪ran⁡H⊆c
25 24 anim1d ⊢KCB⊆c→so∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→so∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K
26 25 imim1d ⊢KCB⊆c→so∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c→so∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
27 26 ralimdv ⊢KCB⊆c→∀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⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
28 27 imim2d ⊢KCB⊆c→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⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
29 28 alimdv ⊢KCB⊆c→∀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⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
30 29 2alimdv ⊢KCB⊆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→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
31 30 com12 ⊢∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆c∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c→KCB⊆c→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
32 31 adantl ⊢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→KCB⊆c→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
33 22 32 sylcom ⊢φ→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→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c
34 eqid ⊢mPreSt⁡T=mPreSt⁡T
35 eqid ⊢mStat⁡T=mStat⁡T
36 34 35 mstapst ⊢mStat⁡T⊆mPreSt⁡T
37 7 35 maxsta ⊢T∈mFS→A⊆mStat⁡T
38 4 37 syl ⊢φ→A⊆mStat⁡T
39 38 12 sseldd ⊢φ→MOP∈mStat⁡T
40 36 39 sselid ⊢φ→MOP∈mPreSt⁡T
41 34 mpstrcl ⊢MOP∈mPreSt⁡T→M∈V∧O∈V∧P∈V
42 simp1 ⊢m=M∧o=O∧p=P→m=M
43 simp2 ⊢m=M∧o=O∧p=P→o=O
44 simp3 ⊢m=M∧o=O∧p=P→p=P
45 42 43 44 oteq123d ⊢m=M∧o=O∧p=P→mop=MOP
46 45 eleq1d ⊢m=M∧o=O∧p=P→mop∈A↔MOP∈A
47 43 uneq1d ⊢m=M∧o=O∧p=P→o∪ran⁡H=O∪ran⁡H
48 47 imaeq2d ⊢m=M∧o=O∧p=P→so∪ran⁡H=sO∪ran⁡H
49 48 sseq1d ⊢m=M∧o=O∧p=P→so∪ran⁡H⊆KCB↔sO∪ran⁡H⊆KCB
50 42 breqd ⊢m=M∧o=O∧p=P→xmy↔xMy
51 50 imbi1d ⊢m=M∧o=O∧p=P→xmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔xMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K
52 51 2albidv ⊢m=M∧o=O∧p=P→∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K
53 49 52 anbi12d ⊢m=M∧o=O∧p=P→so∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔sO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K
54 44 fveq2d ⊢m=M∧o=O∧p=P→s⁡p=s⁡P
55 54 eleq1d ⊢m=M∧o=O∧p=P→s⁡p∈c↔s⁡P∈c
56 53 55 imbi12d ⊢m=M∧o=O∧p=P→so∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔sO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c
57 56 ralbidv ⊢m=M∧o=O∧p=P→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c
58 46 57 imbi12d ⊢m=M∧o=O∧p=P→mop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c↔MOP∈A→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c
59 58 spc3gv ⊢M∈V∧O∈V∧P∈V→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c→MOP∈A→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c
60 40 41 59 3syl ⊢φ→∀m∀o∀pmop∈A→∀s∈ran⁡Lso∪ran⁡H⊆KCB∧∀x∀yxmy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡p∈c→MOP∈A→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c
61 elun ⊢x∈O∪ran⁡H↔x∈O∨x∈ran⁡H
62 15 ralrimiva ⊢φ→∀v∈VS⁡H⁡v∈KCB
63 9 2 10 mvhf ⊢T∈mFS→H:V⟶E
64 4 63 syl ⊢φ→H:V⟶E
65 ffn ⊢H:V⟶E→HFnV
66 fveq2 ⊢x=H⁡v→S⁡x=S⁡H⁡v
67 66 eleq1d ⊢x=H⁡v→S⁡x∈KCB↔S⁡H⁡v∈KCB
68 67 ralrn ⊢HFnV→∀x∈ran⁡HS⁡x∈KCB↔∀v∈VS⁡H⁡v∈KCB
69 64 65 68 3syl ⊢φ→∀x∈ran⁡HS⁡x∈KCB↔∀v∈VS⁡H⁡v∈KCB
70 62 69 mpbird ⊢φ→∀x∈ran⁡HS⁡x∈KCB
71 70 r19.21bi ⊢φ∧x∈ran⁡H→S⁡x∈KCB
72 14 71 jaodan ⊢φ∧x∈O∨x∈ran⁡H→S⁡x∈KCB
73 61 72 sylan2b ⊢φ∧x∈O∪ran⁡H→S⁡x∈KCB
74 73 ralrimiva ⊢φ→∀x∈O∪ran⁡HS⁡x∈KCB
75 8 2 msubf ⊢S∈ran⁡L→S:E⟶E
76 13 75 syl ⊢φ→S:E⟶E
77 76 ffund ⊢φ→Fun⁡S
78 1 2 34 elmpst ⊢MOP∈mPreSt⁡T↔M⊆D∧M-1=M∧O⊆E∧O∈Fin∧P∈E
79 40 78 sylib ⊢φ→M⊆D∧M-1=M∧O⊆E∧O∈Fin∧P∈E
80 79 simp2d ⊢φ→O⊆E∧O∈Fin
81 80 simpld ⊢φ→O⊆E
82 76 fdmd ⊢φ→dom⁡S=E
83 81 82 sseqtrrd ⊢φ→O⊆dom⁡S
84 64 frnd ⊢φ→ran⁡H⊆E
85 84 82 sseqtrrd ⊢φ→ran⁡H⊆dom⁡S
86 83 85 unssd ⊢φ→O∪ran⁡H⊆dom⁡S
87 funimass4 ⊢Fun⁡S∧O∪ran⁡H⊆dom⁡S→SO∪ran⁡H⊆KCB↔∀x∈O∪ran⁡HS⁡x∈KCB
88 77 86 87 syl2anc ⊢φ→SO∪ran⁡H⊆KCB↔∀x∈O∪ran⁡HS⁡x∈KCB
89 74 88 mpbird ⊢φ→SO∪ran⁡H⊆KCB
90 16 3exp2 ⊢φ→xMy→a∈W⁡S⁡H⁡x→b∈W⁡S⁡H⁡y→aKb
91 90 imp4b ⊢φ∧xMy→a∈W⁡S⁡H⁡x∧b∈W⁡S⁡H⁡y→aKb
92 91 ralrimivv ⊢φ∧xMy→∀a∈W⁡S⁡H⁡x∀b∈W⁡S⁡H⁡yaKb
93 dfss3 ⊢W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K↔∀z∈W⁡S⁡H⁡x×W⁡S⁡H⁡yz∈K
94 eleq1 ⊢z=ab→z∈K↔ab∈K
95 df-br ⊢aKb↔ab∈K
96 94 95 bitr4di ⊢z=ab→z∈K↔aKb
97 96 ralxp ⊢∀z∈W⁡S⁡H⁡x×W⁡S⁡H⁡yz∈K↔∀a∈W⁡S⁡H⁡x∀b∈W⁡S⁡H⁡yaKb
98 93 97 bitri ⊢W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K↔∀a∈W⁡S⁡H⁡x∀b∈W⁡S⁡H⁡yaKb
99 92 98 sylibr ⊢φ∧xMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
100 99 ex ⊢φ→xMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
101 100 alrimivv ⊢φ→∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
102 89 101 jca ⊢φ→SO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
103 imaeq1 ⊢s=S→sO∪ran⁡H=SO∪ran⁡H
104 103 sseq1d ⊢s=S→sO∪ran⁡H⊆KCB↔SO∪ran⁡H⊆KCB
105 fveq1 ⊢s=S→s⁡H⁡x=S⁡H⁡x
106 105 fveq2d ⊢s=S→W⁡s⁡H⁡x=W⁡S⁡H⁡x
107 fveq1 ⊢s=S→s⁡H⁡y=S⁡H⁡y
108 107 fveq2d ⊢s=S→W⁡s⁡H⁡y=W⁡S⁡H⁡y
109 106 108 xpeq12d ⊢s=S→W⁡s⁡H⁡x×W⁡s⁡H⁡y=W⁡S⁡H⁡x×W⁡S⁡H⁡y
110 109 sseq1d ⊢s=S→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
111 110 imbi2d ⊢s=S→xMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔xMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
112 111 2albidv ⊢s=S→∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
113 104 112 anbi12d ⊢s=S→sO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K↔SO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K
114 fveq1 ⊢s=S→s⁡P=S⁡P
115 114 eleq1d ⊢s=S→s⁡P∈c↔S⁡P∈c
116 113 115 imbi12d ⊢s=S→sO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c↔SO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K→S⁡P∈c
117 116 rspcv ⊢S∈ran⁡L→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c→SO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K→S⁡P∈c
118 13 117 syl ⊢φ→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c→SO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡S⁡H⁡x×W⁡S⁡H⁡y⊆K→S⁡P∈c
119 102 118 mpid ⊢φ→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c→S⁡P∈c
120 12 119 embantd ⊢φ→MOP∈A→∀s∈ran⁡LsO∪ran⁡H⊆KCB∧∀x∀yxMy→W⁡s⁡H⁡x×W⁡s⁡H⁡y⊆K→s⁡P∈c→S⁡P∈c
121 33 60 120 3syld ⊢φ→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→S⁡P∈c
122 121 alrimiv ⊢φ→∀cB∪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→S⁡P∈c
123 fvex ⊢S⁡P∈V
124 123 elintab ⊢S⁡P∈⋂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↔∀cB∪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→S⁡P∈c
125 122 124 sylibr ⊢φ→S⁡P∈⋂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
126 125 20 eleqtrrd ⊢φ→S⁡P∈KCB