# 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}=\mathrm{mDV}\left({T}\right)$
mclsval.e ${⊢}{E}=\mathrm{mEx}\left({T}\right)$
mclsval.c ${⊢}{C}=\mathrm{mCls}\left({T}\right)$
mclsval.1 ${⊢}{\phi }\to {T}\in \mathrm{mFS}$
mclsval.2 ${⊢}{\phi }\to {K}\subseteq {D}$
mclsval.3 ${⊢}{\phi }\to {B}\subseteq {E}$
mclsax.a ${⊢}{A}=\mathrm{mAx}\left({T}\right)$
mclsax.l ${⊢}{L}=\mathrm{mSubst}\left({T}\right)$
mclsax.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
mclsax.h ${⊢}{H}=\mathrm{mVH}\left({T}\right)$
mclsax.w ${⊢}{W}=\mathrm{mVars}\left({T}\right)$
mclsax.4 ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in {A}$
mclsax.5 ${⊢}{\phi }\to {S}\in \mathrm{ran}{L}$
mclsax.6 ${⊢}\left({\phi }\wedge {x}\in {O}\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
mclsax.7 ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)$
mclsax.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 mclsax ${⊢}{\phi }\to {S}\left({P}\right)\in \left({K}{C}{B}\right)$

### Proof

Step Hyp Ref Expression
1 mclsval.d ${⊢}{D}=\mathrm{mDV}\left({T}\right)$
2 mclsval.e ${⊢}{E}=\mathrm{mEx}\left({T}\right)$
3 mclsval.c ${⊢}{C}=\mathrm{mCls}\left({T}\right)$
4 mclsval.1 ${⊢}{\phi }\to {T}\in \mathrm{mFS}$
5 mclsval.2 ${⊢}{\phi }\to {K}\subseteq {D}$
6 mclsval.3 ${⊢}{\phi }\to {B}\subseteq {E}$
7 mclsax.a ${⊢}{A}=\mathrm{mAx}\left({T}\right)$
8 mclsax.l ${⊢}{L}=\mathrm{mSubst}\left({T}\right)$
9 mclsax.v ${⊢}{V}=\mathrm{mVR}\left({T}\right)$
10 mclsax.h ${⊢}{H}=\mathrm{mVH}\left({T}\right)$
11 mclsax.w ${⊢}{W}=\mathrm{mVars}\left({T}\right)$
12 mclsax.4 ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in {A}$
13 mclsax.5 ${⊢}{\phi }\to {S}\in \mathrm{ran}{L}$
14 mclsax.6 ${⊢}\left({\phi }\wedge {x}\in {O}\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
15 mclsax.7 ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)$
16 mclsax.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 abid ${⊢}{c}\in \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}↔\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
18 intss1 ${⊢}{c}\in \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}\to \bigcap \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}\subseteq {c}$
19 17 18 sylbir ${⊢}\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to \bigcap \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}\subseteq {c}$
20 1 2 3 4 5 6 10 7 8 11 mclsval ${⊢}{\phi }\to {K}{C}{B}=\bigcap \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}$
21 20 sseq1d ${⊢}{\phi }\to \left({K}{C}{B}\subseteq {c}↔\bigcap \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}\subseteq {c}\right)$
22 19 21 syl5ibr ${⊢}{\phi }\to \left(\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to {K}{C}{B}\subseteq {c}\right)$
23 sstr2 ${⊢}{s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\to \left({K}{C}{B}\subseteq {c}\to {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\right)$
24 23 com12 ${⊢}{K}{C}{B}\subseteq {c}\to \left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\to {s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\right)$
25 24 anim1d ${⊢}{K}{C}{B}\subseteq {c}\to \left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to \left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\right)$
26 25 imim1d ${⊢}{K}{C}{B}\subseteq {c}\to \left(\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\to \left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)$
27 26 ralimdv ${⊢}{K}{C}{B}\subseteq {c}\to \left(\forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)$
28 27 imim2d ${⊢}{K}{C}{B}\subseteq {c}\to \left(\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\to \left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
29 28 alimdv ${⊢}{K}{C}{B}\subseteq {c}\to \left(\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\to \forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
30 29 2alimdv ${⊢}{K}{C}{B}\subseteq {c}\to \left(\forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\to \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
31 30 com12 ${⊢}\forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\to \left({K}{C}{B}\subseteq {c}\to \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
32 31 adantl ${⊢}\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to \left({K}{C}{B}\subseteq {c}\to \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
33 22 32 sylcom ${⊢}{\phi }\to \left(\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)$
34 eqid ${⊢}\mathrm{mPreSt}\left({T}\right)=\mathrm{mPreSt}\left({T}\right)$
35 eqid ${⊢}\mathrm{mStat}\left({T}\right)=\mathrm{mStat}\left({T}\right)$
36 34 35 mstapst ${⊢}\mathrm{mStat}\left({T}\right)\subseteq \mathrm{mPreSt}\left({T}\right)$
37 7 35 maxsta ${⊢}{T}\in \mathrm{mFS}\to {A}\subseteq \mathrm{mStat}\left({T}\right)$
38 4 37 syl ${⊢}{\phi }\to {A}\subseteq \mathrm{mStat}\left({T}\right)$
39 38 12 sseldd ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in \mathrm{mStat}\left({T}\right)$
40 36 39 sseldi ${⊢}{\phi }\to ⟨{M},{O},{P}⟩\in \mathrm{mPreSt}\left({T}\right)$
41 34 mpstrcl ${⊢}⟨{M},{O},{P}⟩\in \mathrm{mPreSt}\left({T}\right)\to \left({M}\in \mathrm{V}\wedge {O}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)$
42 simp1 ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to {m}={M}$
43 simp2 ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to {o}={O}$
44 simp3 ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to {p}={P}$
45 42 43 44 oteq123d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to ⟨{m},{o},{p}⟩=⟨{M},{O},{P}⟩$
46 45 eleq1d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(⟨{m},{o},{p}⟩\in {A}↔⟨{M},{O},{P}⟩\in {A}\right)$
47 43 uneq1d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to {o}\cup \mathrm{ran}{H}={O}\cup \mathrm{ran}{H}$
48 47 imaeq2d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to {s}\left[{o}\cup \mathrm{ran}{H}\right]={s}\left[{O}\cup \mathrm{ran}{H}\right]$
49 48 sseq1d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}↔{s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\right)$
50 42 breqd ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left({x}{m}{y}↔{x}{M}{y}\right)$
51 50 imbi1d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)↔\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)$
52 51 2albidv ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)$
53 49 52 anbi12d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)↔\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\right)$
54 44 fveq2d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to {s}\left({p}\right)={s}\left({P}\right)$
55 54 eleq1d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left({s}\left({p}\right)\in {c}↔{s}\left({P}\right)\in {c}\right)$
56 53 55 imbi12d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)↔\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\right)$
57 56 ralbidv ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(\forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)↔\forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\right)$
58 46 57 imbi12d ${⊢}\left({m}={M}\wedge {o}={O}\wedge {p}={P}\right)\to \left(\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)↔\left(⟨{M},{O},{P}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\right)\right)$
59 58 spc3gv ${⊢}\left({M}\in \mathrm{V}\wedge {O}\in \mathrm{V}\wedge {P}\in \mathrm{V}\right)\to \left(\forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\to \left(⟨{M},{O},{P}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\right)\right)$
60 40 41 59 3syl ${⊢}{\phi }\to \left(\forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\to \left(⟨{M},{O},{P}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\right)\right)$
61 elun ${⊢}{x}\in \left({O}\cup \mathrm{ran}{H}\right)↔\left({x}\in {O}\vee {x}\in \mathrm{ran}{H}\right)$
62 15 ralrimiva ${⊢}{\phi }\to \forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)$
63 9 2 10 mvhf ${⊢}{T}\in \mathrm{mFS}\to {H}:{V}⟶{E}$
64 4 63 syl ${⊢}{\phi }\to {H}:{V}⟶{E}$
65 ffn ${⊢}{H}:{V}⟶{E}\to {H}Fn{V}$
66 fveq2 ${⊢}{x}={H}\left({v}\right)\to {S}\left({x}\right)={S}\left({H}\left({v}\right)\right)$
67 66 eleq1d ${⊢}{x}={H}\left({v}\right)\to \left({S}\left({x}\right)\in \left({K}{C}{B}\right)↔{S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)\right)$
68 67 ralrn ${⊢}{H}Fn{V}\to \left(\forall {x}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)\right)$
69 64 65 68 3syl ${⊢}{\phi }\to \left(\forall {x}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)↔\forall {v}\in {V}\phantom{\rule{.4em}{0ex}}{S}\left({H}\left({v}\right)\right)\in \left({K}{C}{B}\right)\right)$
70 62 69 mpbird ${⊢}{\phi }\to \forall {x}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)$
71 70 r19.21bi ${⊢}\left({\phi }\wedge {x}\in \mathrm{ran}{H}\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
72 14 71 jaodan ${⊢}\left({\phi }\wedge \left({x}\in {O}\vee {x}\in \mathrm{ran}{H}\right)\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
73 61 72 sylan2b ${⊢}\left({\phi }\wedge {x}\in \left({O}\cup \mathrm{ran}{H}\right)\right)\to {S}\left({x}\right)\in \left({K}{C}{B}\right)$
74 73 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left({O}\cup \mathrm{ran}{H}\right)\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)$
75 8 2 msubf ${⊢}{S}\in \mathrm{ran}{L}\to {S}:{E}⟶{E}$
76 13 75 syl ${⊢}{\phi }\to {S}:{E}⟶{E}$
77 76 ffund ${⊢}{\phi }\to \mathrm{Fun}{S}$
78 1 2 34 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)$
79 40 78 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)$
80 79 simp2d ${⊢}{\phi }\to \left({O}\subseteq {E}\wedge {O}\in \mathrm{Fin}\right)$
81 80 simpld ${⊢}{\phi }\to {O}\subseteq {E}$
82 76 fdmd ${⊢}{\phi }\to \mathrm{dom}{S}={E}$
83 81 82 sseqtrrd ${⊢}{\phi }\to {O}\subseteq \mathrm{dom}{S}$
84 64 frnd ${⊢}{\phi }\to \mathrm{ran}{H}\subseteq {E}$
85 84 82 sseqtrrd ${⊢}{\phi }\to \mathrm{ran}{H}\subseteq \mathrm{dom}{S}$
86 83 85 unssd ${⊢}{\phi }\to {O}\cup \mathrm{ran}{H}\subseteq \mathrm{dom}{S}$
87 funimass4 ${⊢}\left(\mathrm{Fun}{S}\wedge {O}\cup \mathrm{ran}{H}\subseteq \mathrm{dom}{S}\right)\to \left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}↔\forall {x}\in \left({O}\cup \mathrm{ran}{H}\right)\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)\right)$
88 77 86 87 syl2anc ${⊢}{\phi }\to \left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}↔\forall {x}\in \left({O}\cup \mathrm{ran}{H}\right)\phantom{\rule{.4em}{0ex}}{S}\left({x}\right)\in \left({K}{C}{B}\right)\right)$
89 74 88 mpbird ${⊢}{\phi }\to {S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}$
90 16 3exp2 ${⊢}{\phi }\to \left({x}{M}{y}\to \left({a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\to \left({b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\to {a}{K}{b}\right)\right)\right)$
91 90 imp4b ${⊢}\left({\phi }\wedge {x}{M}{y}\right)\to \left(\left({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)\to {a}{K}{b}\right)$
92 91 ralrimivv ${⊢}\left({\phi }\wedge {x}{M}{y}\right)\to \forall {a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{a}{K}{b}$
93 dfss3 ${⊢}{W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}↔\forall {z}\in \left({W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{z}\in {K}$
94 eleq1 ${⊢}{z}=⟨{a},{b}⟩\to \left({z}\in {K}↔⟨{a},{b}⟩\in {K}\right)$
95 df-br ${⊢}{a}{K}{b}↔⟨{a},{b}⟩\in {K}$
96 94 95 syl6bbr ${⊢}{z}=⟨{a},{b}⟩\to \left({z}\in {K}↔{a}{K}{b}\right)$
97 96 ralxp ${⊢}\forall {z}\in \left({W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\right)\phantom{\rule{.4em}{0ex}}{z}\in {K}↔\forall {a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{a}{K}{b}$
98 93 97 bitri ${⊢}{W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}↔\forall {a}\in {W}\left({S}\left({H}\left({x}\right)\right)\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in {W}\left({S}\left({H}\left({y}\right)\right)\right)\phantom{\rule{.4em}{0ex}}{a}{K}{b}$
99 92 98 sylibr ${⊢}\left({\phi }\wedge {x}{M}{y}\right)\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}$
100 99 ex ${⊢}{\phi }\to \left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)$
101 100 alrimivv ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)$
102 89 101 jca ${⊢}{\phi }\to \left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)$
103 imaeq1 ${⊢}{s}={S}\to {s}\left[{O}\cup \mathrm{ran}{H}\right]={S}\left[{O}\cup \mathrm{ran}{H}\right]$
104 103 sseq1d ${⊢}{s}={S}\to \left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}↔{S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\right)$
105 fveq1 ${⊢}{s}={S}\to {s}\left({H}\left({x}\right)\right)={S}\left({H}\left({x}\right)\right)$
106 105 fveq2d ${⊢}{s}={S}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)={W}\left({S}\left({H}\left({x}\right)\right)\right)$
107 fveq1 ${⊢}{s}={S}\to {s}\left({H}\left({y}\right)\right)={S}\left({H}\left({y}\right)\right)$
108 107 fveq2d ${⊢}{s}={S}\to {W}\left({s}\left({H}\left({y}\right)\right)\right)={W}\left({S}\left({H}\left({y}\right)\right)\right)$
109 106 108 xpeq12d ${⊢}{s}={S}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)={W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)$
110 109 sseq1d ${⊢}{s}={S}\to \left({W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}↔{W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)$
111 110 imbi2d ${⊢}{s}={S}\to \left(\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)↔\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)$
112 111 2albidv ${⊢}{s}={S}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)$
113 104 112 anbi12d ${⊢}{s}={S}\to \left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)↔\left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\right)$
114 fveq1 ${⊢}{s}={S}\to {s}\left({P}\right)={S}\left({P}\right)$
115 114 eleq1d ${⊢}{s}={S}\to \left({s}\left({P}\right)\in {c}↔{S}\left({P}\right)\in {c}\right)$
116 113 115 imbi12d ${⊢}{s}={S}\to \left(\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)↔\left(\left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {S}\left({P}\right)\in {c}\right)\right)$
117 116 rspcv ${⊢}{S}\in \mathrm{ran}{L}\to \left(\forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\to \left(\left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {S}\left({P}\right)\in {c}\right)\right)$
118 13 117 syl ${⊢}{\phi }\to \left(\forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\to \left(\left({S}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({S}\left({H}\left({x}\right)\right)\right)×{W}\left({S}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {S}\left({P}\right)\in {c}\right)\right)$
119 102 118 mpid ${⊢}{\phi }\to \left(\forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\to {S}\left({P}\right)\in {c}\right)$
120 12 119 embantd ${⊢}{\phi }\to \left(\left(⟨{M},{O},{P}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{O}\cup \mathrm{ran}{H}\right]\subseteq {K}{C}{B}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{M}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({P}\right)\in {c}\right)\right)\to {S}\left({P}\right)\in {c}\right)$
121 33 60 120 3syld ${⊢}{\phi }\to \left(\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to {S}\left({P}\right)\in {c}\right)$
122 121 alrimiv ${⊢}{\phi }\to \forall {c}\phantom{\rule{.4em}{0ex}}\left(\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to {S}\left({P}\right)\in {c}\right)$
123 fvex ${⊢}{S}\left({P}\right)\in \mathrm{V}$
124 123 elintab ${⊢}{S}\left({P}\right)\in \bigcap \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}↔\forall {c}\phantom{\rule{.4em}{0ex}}\left(\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\to {S}\left({P}\right)\in {c}\right)$
125 122 124 sylibr ${⊢}{\phi }\to {S}\left({P}\right)\in \bigcap \left\{{c}|\left({B}\cup \mathrm{ran}{H}\subseteq {c}\wedge \forall {m}\phantom{\rule{.4em}{0ex}}\forall {o}\phantom{\rule{.4em}{0ex}}\forall {p}\phantom{\rule{.4em}{0ex}}\left(⟨{m},{o},{p}⟩\in {A}\to \forall {s}\in \mathrm{ran}{L}\phantom{\rule{.4em}{0ex}}\left(\left({s}\left[{o}\cup \mathrm{ran}{H}\right]\subseteq {c}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}{m}{y}\to {W}\left({s}\left({H}\left({x}\right)\right)\right)×{W}\left({s}\left({H}\left({y}\right)\right)\right)\subseteq {K}\right)\right)\to {s}\left({p}\right)\in {c}\right)\right)\right)\right\}$
126 125 20 eleqtrrd ${⊢}{\phi }\to {S}\left({P}\right)\in \left({K}{C}{B}\right)$