# Metamath Proof Explorer

## Theorem mclspps

Description: The closure is closed under application of provable pre-statements. (Compare mclsax .) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclspps.d ${⊢}{D}=\mathrm{mDV}\left({T}\right)$
mclspps.e ${⊢}{E}=\mathrm{mEx}\left({T}\right)$
mclspps.c ${⊢}{C}=\mathrm{mCls}\left({T}\right)$
mclspps.1 ${⊢}{\phi }\to {T}\in \mathrm{mFS}$
mclspps.2 ${⊢}{\phi }\to {K}\subseteq {D}$
mclspps.3 ${⊢}{\phi }\to {B}\subseteq {E}$
mclspps.j ${⊢}{J}=\mathrm{mPPSt}\left({T}\right)$
mclspps.l ${⊢}{L}=\mathrm{mSubst}\left({T}\right)$
mclspps.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
mclspps.h ${⊢}{H}=\mathrm{mVH}\left({T}\right)$
mclspps.w ${⊢}{W}=\mathrm{mVars}\left({T}\right)$
mclspps.4 ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in {J}$
mclspps.5 ${⊢}{\phi }\to {S}\in \mathrm{ran}{L}$
mclspps.6 ${⊢}\left({\phi }\wedge {x}\in {O}\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
mclspps.7 ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)$
mclspps.8 ${⊢}\left({\phi }\wedge \left({x}{M}{y}\wedge {a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\wedge {b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\right)\right)\to {a}{K}{b}$
Assertion mclspps ${⊢}{\phi }\to {S}\left({P}\right)\in \left({K}{C}{B}\right)$

### Proof

Step Hyp Ref Expression
1 mclspps.d ${⊢}{D}=\mathrm{mDV}\left({T}\right)$
2 mclspps.e ${⊢}{E}=\mathrm{mEx}\left({T}\right)$
3 mclspps.c ${⊢}{C}=\mathrm{mCls}\left({T}\right)$
4 mclspps.1 ${⊢}{\phi }\to {T}\in \mathrm{mFS}$
5 mclspps.2 ${⊢}{\phi }\to {K}\subseteq {D}$
6 mclspps.3 ${⊢}{\phi }\to {B}\subseteq {E}$
7 mclspps.j ${⊢}{J}=\mathrm{mPPSt}\left({T}\right)$
8 mclspps.l ${⊢}{L}=\mathrm{mSubst}\left({T}\right)$
9 mclspps.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
10 mclspps.h ${⊢}{H}=\mathrm{mVH}\left({T}\right)$
11 mclspps.w ${⊢}{W}=\mathrm{mVars}\left({T}\right)$
12 mclspps.4 ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in {J}$
13 mclspps.5 ${⊢}{\phi }\to {S}\in \mathrm{ran}{L}$
14 mclspps.6 ${⊢}\left({\phi }\wedge {x}\in {O}\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
15 mclspps.7 ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)$
16 mclspps.8 ${⊢}\left({\phi }\wedge \left({x}{M}{y}\wedge {a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\wedge {b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\right)\right)\to {a}{K}{b}$
17 8 2 msubf ${⊢}{S}\in \mathrm{ran}{L}\to {S}:{E}⟶{E}$
18 13 17 syl ${⊢}{\phi }\to {S}:{E}⟶{E}$
19 18 ffnd ${⊢}{\phi }\to {S}Fn{E}$
20 eqid ${⊢}\mathrm{mPreSt}\left({T}\right)=\mathrm{mPreSt}\left({T}\right)$
21 20 7 mppspst ${⊢}{J}\subseteq \mathrm{mPreSt}\left({T}\right)$
22 21 12 sseldi ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in \mathrm{mPreSt}\left({T}\right)$
23 1 2 20 elmpst ${⊢}⟨{M},{O},{P}⟩\in \mathrm{mPreSt}\left({T}\right)↔\left(\left({M}\subseteq {D}\wedge {{M}}^{-1}={M}\right)\wedge \left({O}\subseteq {E}\wedge {O}\in \mathrm{Fin}\right)\wedge {P}\in {E}\right)$
24 22 23 sylib ${⊢}{\phi }\to \left(\left({M}\subseteq {D}\wedge {{M}}^{-1}={M}\right)\wedge \left({O}\subseteq {E}\wedge {O}\in \mathrm{Fin}\right)\wedge {P}\in {E}\right)$
25 24 simp1d ${⊢}{\phi }\to \left({M}\subseteq {D}\wedge {{M}}^{-1}={M}\right)$
26 25 simpld ${⊢}{\phi }\to {M}\subseteq {D}$
27 24 simp2d ${⊢}{\phi }\to \left({O}\subseteq {E}\wedge {O}\in \mathrm{Fin}\right)$
28 27 simpld ${⊢}{\phi }\to {O}\subseteq {E}$
29 eqid ${⊢}\mathrm{mAx}\left({T}\right)=\mathrm{mAx}\left({T}\right)$
30 14 ralrimiva ${⊢}{\phi }\to \forall {x}\in {O}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)$
31 18 ffund ${⊢}{\phi }\to \mathrm{Fun}{S}$
32 18 fdmd ${⊢}{\phi }\to \mathrm{dom}{S}={E}$
33 28 32 sseqtrrd ${⊢}{\phi }\to {O}\subseteq \mathrm{dom}{S}$
34 funimass5 ${⊢}\left(\mathrm{Fun}{S}\wedge {O}\subseteq \mathrm{dom}{S}\right)\to \left({O}\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]↔\forall {x}\in {O}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)\right)$
35 31 33 34 syl2anc ${⊢}{\phi }\to \left({O}\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]↔\forall {x}\in {O}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)\right)$
36 30 35 mpbird ${⊢}{\phi }\to {O}\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]$
37 9 2 10 mvhf ${⊢}{T}\in \mathrm{mFS}\to {H}:{V}⟶{E}$
38 4 37 syl ${⊢}{\phi }\to {H}:{V}⟶{E}$
39 38 ffvelrnda ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {H}\left({v}\right)\in {E}$
40 elpreima ${⊢}{S}Fn{E}\to \left({H}\left({v}\right)\in {{S}}^{-1}\left[{K}{C}{B}\right]↔\left({H}\left({v}\right)\in {E}\wedge {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)\right)\right)$
41 19 40 syl ${⊢}{\phi }\to \left({H}\left({v}\right)\in {{S}}^{-1}\left[{K}{C}{B}\right]↔\left({H}\left({v}\right)\in {E}\wedge {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)\right)\right)$
42 41 adantr ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to \left({H}\left({v}\right)\in {{S}}^{-1}\left[{K}{C}{B}\right]↔\left({H}\left({v}\right)\in {E}\wedge {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)\right)\right)$
43 39 15 42 mpbir2and ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {H}\left({v}\right)\in {{S}}^{-1}\left[{K}{C}{B}\right]$
44 4 3ad2ant1 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {T}\in \mathrm{mFS}$
45 5 3ad2ant1 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {K}\subseteq {D}$
46 6 3ad2ant1 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {B}\subseteq {E}$
47 12 3ad2ant1 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to ⟨{M},{O},{P}⟩\in {J}$
48 13 3ad2ant1 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {S}\in \mathrm{ran}{L}$
49 14 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\wedge {x}\in {O}\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
50 15 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\wedge {v}\in {V}\right)\to {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)$
51 16 3ad2antl1 ${⊢}\left(\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\wedge \left({x}{M}{y}\wedge {a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\wedge {b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\right)\right)\to {a}{K}{b}$
52 simp21 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to ⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)$
53 simp22 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {s}\in \mathrm{ran}{L}$
54 simp23 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]$
55 simp3 ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)$
56 1 2 3 44 45 46 7 8 9 10 11 47 48 49 50 51 52 53 54 55 mclsppslem ${⊢}\left({\phi }\wedge \left(⟨{m},{o},{p}⟩\in \mathrm{mAx}\left({T}\right)\wedge {s}\in \mathrm{ran}{L}\wedge {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]\right)\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}{m}{w}\to {W}\left({s}\left({H}\left({z}\right)\right)\right)×{W}\left({s}\left({H}\left({w}\right)\right)\right)\subseteq {M}\right)\right)\to {s}\left({p}\right)\in {{S}}^{-1}\left[{K}{C}{B}\right]$
57 1 2 3 4 26 28 29 8 9 10 11 36 43 56 mclsind ${⊢}{\phi }\to {M}{C}{O}\subseteq {{S}}^{-1}\left[{K}{C}{B}\right]$
58 20 7 3 elmpps ${⊢}⟨{M},{O},{P}⟩\in {J}↔\left(⟨{M},{O},{P}⟩\in \mathrm{mPreSt}\left({T}\right)\wedge {P}\in \left({M}{C}{O}\right)\right)$
59 58 simprbi ${⊢}⟨{M},{O},{P}⟩\in {J}\to {P}\in \left({M}{C}{O}\right)$
60 12 59 syl ${⊢}{\phi }\to {P}\in \left({M}{C}{O}\right)$
61 57 60 sseldd ${⊢}{\phi }\to {P}\in {{S}}^{-1}\left[{K}{C}{B}\right]$
62 elpreima ${⊢}{S}Fn{E}\to \left({P}\in {{S}}^{-1}\left[{K}{C}{B}\right]↔\left({P}\in {E}\wedge {S}\left({P}\right)\in \left({K}{C}{B}\right)\right)\right)$
63 62 simplbda ${⊢}\left({S}Fn{E}\wedge {P}\in {{S}}^{-1}\left[{K}{C}{B}\right]\right)\to {S}\left({P}\right)\in \left({K}{C}{B}\right)$
64 19 61 63 syl2anc ${⊢}{\phi }\to {S}\left({P}\right)\in \left({K}{C}{B}\right)$