Theorem mclsax 35883

Description: The closure is closed under axiom application. (Contributed by Mario Carneiro, 18-Jul-2016.)

Hypotheses

Ref	Expression
mclsval.d	⊢ 𝐷 = (mDV‘𝑇)
mclsval.e	⊢ 𝐸 = (mEx‘𝑇)
mclsval.c	⊢ 𝐶 = (mCls‘𝑇)
mclsval.1	⊢ (𝜑 → 𝑇 ∈ mFS)
mclsval.2	⊢ (𝜑 → 𝐾 ⊆ 𝐷)
mclsval.3	⊢ (𝜑 → 𝐵 ⊆ 𝐸)
mclsax.a	⊢ 𝐴 = (mAx‘𝑇)
mclsax.l	⊢ 𝐿 = (mSubst‘𝑇)
mclsax.v	⊢ 𝑉 = (mVR‘𝑇)
mclsax.h	⊢ 𝐻 = (mVH‘𝑇)
mclsax.w	⊢ 𝑊 = (mVars‘𝑇)
mclsax.4	⊢ (𝜑 → ⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴)
mclsax.5	⊢ (𝜑 → 𝑆 ∈ ran 𝐿)
mclsax.6	⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
mclsax.7	⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))
mclsax.8	⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏)

Assertion

Ref	Expression
mclsax	⊢ (𝜑 → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵))

Distinct variable groups:   𝑣,𝐸   𝑎,𝑏,𝑣,𝑥,𝐻   𝑦,𝑣,𝐵,𝑥   𝑣,𝐶,𝑥   𝑥,𝐿,𝑦   𝑥,𝑂,𝑦   𝑦,𝑎,𝑆,𝑏,𝑣,𝑥   𝑀,𝑎,𝑏,𝑥,𝑦   𝑥,𝑃,𝑦   𝑥,𝑇,𝑦   𝜑,𝑎,𝑏,𝑣,𝑥,𝑦   𝑣,𝑉,𝑥   𝑊,𝑎,𝑏,𝑥   𝐾,𝑎,𝑏,𝑣,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑎,𝑏)   𝐵(𝑎,𝑏)   𝐶(𝑦,𝑎,𝑏)   𝐷(𝑥,𝑦,𝑣,𝑎,𝑏)   𝑃(𝑣,𝑎,𝑏)   𝑇(𝑣,𝑎,𝑏)   𝐸(𝑥,𝑦,𝑎,𝑏)   𝐻(𝑦)   𝐿(𝑣,𝑎,𝑏)   𝑀(𝑣)   𝑂(𝑣,𝑎,𝑏)   𝑉(𝑦,𝑎,𝑏)   𝑊(𝑦,𝑣)

Proof of Theorem mclsax

Dummy variables 𝑐 𝑚 𝑜 𝑝 𝑠 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		abid 2743	. . . . . . . 8 ⊢ (𝑐 ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ↔ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
2		intss1 4920	. . . . . . . 8 ⊢ (𝑐 ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑐)
3	1, 2	sylbir 237	. . . . . . 7 ⊢ (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑐)
4		mclsval.d	. . . . . . . . 9 ⊢ 𝐷 = (mDV‘𝑇)
5		mclsval.e	. . . . . . . . 9 ⊢ 𝐸 = (mEx‘𝑇)
6		mclsval.c	. . . . . . . . 9 ⊢ 𝐶 = (mCls‘𝑇)
7		mclsval.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ mFS)
8		mclsval.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ⊆ 𝐷)
9		mclsval.3	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ⊆ 𝐸)
10		mclsax.h	. . . . . . . . 9 ⊢ 𝐻 = (mVH‘𝑇)
11		mclsax.a	. . . . . . . . 9 ⊢ 𝐴 = (mAx‘𝑇)
12		mclsax.l	. . . . . . . . 9 ⊢ 𝐿 = (mSubst‘𝑇)
13		mclsax.w	. . . . . . . . 9 ⊢ 𝑊 = (mVars‘𝑇)
14	4, 5, 6, 7, 8, 9, 10, 11, 12, 13	mclsval 35877	. . . . . . . 8 ⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})
15	14	sseq1d 3967	. . . . . . 7 ⊢ (𝜑 → ((𝐾𝐶𝐵) ⊆ 𝑐 ↔ ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑐))
16	3, 15	imbitrrid 248	. . . . . 6 ⊢ (𝜑 → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝐾𝐶𝐵) ⊆ 𝑐))
17		sstr2 3943	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) → ((𝐾𝐶𝐵) ⊆ 𝑐 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐))
18	17	com12 32	. . . . . . . . . . . . . 14 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐))
19	18	anim1d 620	. . . . . . . . . . . . 13 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾))))
20	19	imim1d 82	. . . . . . . . . . . 12 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))
21	20	ralimdv 3175	. . . . . . . . . . 11 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))
22	21	imim2d 57	. . . . . . . . . 10 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
23	22	alimdv 1935	. . . . . . . . 9 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
24	23	2alimdv 1937	. . . . . . . 8 ⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
25	24	com12 32	. . . . . . 7 ⊢ (∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → ((𝐾𝐶𝐵) ⊆ 𝑐 → ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
26	25	adantl 485	. . . . . 6 ⊢ (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → ((𝐾𝐶𝐵) ⊆ 𝑐 → ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
27	16, 26	sylcom 30	. . . . 5 ⊢ (𝜑 → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
28		eqid 2761	. . . . . . . 8 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
29		eqid 2761	. . . . . . . 8 ⊢ (mStat‘𝑇) = (mStat‘𝑇)
30	28, 29	mstapst 35861	. . . . . . 7 ⊢ (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
31	11, 29	maxsta 35868	. . . . . . . . 9 ⊢ (𝑇 ∈ mFS → 𝐴 ⊆ (mStat‘𝑇))
32	7, 31	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ (mStat‘𝑇))
33		mclsax.4	. . . . . . . 8 ⊢ (𝜑 → ⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴)
34	32, 33	sseldd 3937	. . . . . . 7 ⊢ (𝜑 → ⟨𝑀, 𝑂, 𝑃⟩ ∈ (mStat‘𝑇))
35	30, 34	sselid 3934	. . . . . 6 ⊢ (𝜑 → ⟨𝑀, 𝑂, 𝑃⟩ ∈ (mPreSt‘𝑇))
36	28	mpstrcl 35855	. . . . . 6 ⊢ (⟨𝑀, 𝑂, 𝑃⟩ ∈ (mPreSt‘𝑇) → (𝑀 ∈ V ∧ 𝑂 ∈ V ∧ 𝑃 ∈ V))
37		simp1 1148	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 𝑚 = 𝑀)
38		simp2 1149	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 𝑜 = 𝑂)
39		simp3 1150	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃)
40	37, 38, 39	oteq123d 4845	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ⟨𝑚, 𝑜, 𝑝⟩ = ⟨𝑀, 𝑂, 𝑃⟩)
41	40	eleq1d 2846	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 ↔ ⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴))
42	38	uneq1d 4120	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑜 ∪ ran 𝐻) = (𝑂 ∪ ran 𝐻))
43	42	imaeq2d 6046	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑠 “ (𝑜 ∪ ran 𝐻)) = (𝑠 “ (𝑂 ∪ ran 𝐻)))
44	43	sseq1d 3967	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ (𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵)))
45	37	breqd 5110	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑥𝑚𝑦 ↔ 𝑥𝑀𝑦))
46	45	imbi1d 343	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ (𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))
47	46	2albidv 1942	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))
48	44, 47	anbi12d 641	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) ↔ ((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾))))
49	39	fveq2d 6867	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑠‘𝑝) = (𝑠‘𝑃))
50	49	eleq1d 2846	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((𝑠‘𝑝) ∈ 𝑐 ↔ (𝑠‘𝑃) ∈ 𝑐))
51	48, 50	imbi12d 346	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)))
52	51	ralbidv 3184	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)))
53	41, 52	imbi12d 346	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ (⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐))))
54	53	spc3gv 3563	. . . . . 6 ⊢ ((𝑀 ∈ V ∧ 𝑂 ∈ V ∧ 𝑃 ∈ V) → (∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → (⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐))))
55	35, 36, 54	3syl 18	. . . . 5 ⊢ (𝜑 → (∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → (⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐))))
56		elun 4106	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑂 ∪ ran 𝐻) ↔ (𝑥 ∈ 𝑂 ∨ 𝑥 ∈ ran 𝐻))
57		mclsax.6	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
58		mclsax.7	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))
59	58	ralrimiva 3153	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑣 ∈ 𝑉 (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))
60		mclsax.v	. . . . . . . . . . . . . . . . 17 ⊢ 𝑉 = (mVR‘𝑇)
61	60, 5, 10	mvhf 35872	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
62	7, 61	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:𝑉⟶𝐸)
63		ffn 6687	. . . . . . . . . . . . . . 15 ⊢ (𝐻:𝑉⟶𝐸 → 𝐻 Fn 𝑉)
64		fveq2 6863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝐻‘𝑣) → (𝑆‘𝑥) = (𝑆‘(𝐻‘𝑣)))
65	64	eleq1d 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐻‘𝑣) → ((𝑆‘𝑥) ∈ (𝐾𝐶𝐵) ↔ (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)))
66	65	ralrn 7065	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn 𝑉 → (∀𝑥 ∈ ran 𝐻(𝑆‘𝑥) ∈ (𝐾𝐶𝐵) ↔ ∀𝑣 ∈ 𝑉 (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)))
67	62, 63, 66	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∀𝑥 ∈ ran 𝐻(𝑆‘𝑥) ∈ (𝐾𝐶𝐵) ↔ ∀𝑣 ∈ 𝑉 (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)))
68	59, 67	mpbird 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑥 ∈ ran 𝐻(𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
69	68	r19.21bi 3253	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐻) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
70	57, 69	jaodan 970	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑂 ∨ 𝑥 ∈ ran 𝐻)) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
71	56, 70	sylan2b 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑂 ∪ ran 𝐻)) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
72	71	ralrimiva 3153	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ (𝑂 ∪ ran 𝐻)(𝑆‘𝑥) ∈ (𝐾𝐶𝐵))
73		mclsax.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ ran 𝐿)
74	12, 5	msubf 35846	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ran 𝐿 → 𝑆:𝐸⟶𝐸)
75	73, 74	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:𝐸⟶𝐸)
76	75	ffund 6692	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑆)
77	4, 5, 28	elmpst 35850	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑀, 𝑂, 𝑃⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin) ∧ 𝑃 ∈ 𝐸))
78	35, 77	sylib 220	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin) ∧ 𝑃 ∈ 𝐸))
79	78	simp2d 1155	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin))
80	79	simpld 498	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑂 ⊆ 𝐸)
81	75	fdmd 6698	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝑆 = 𝐸)
82	80, 81	sseqtrrd 3973	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑂 ⊆ dom 𝑆)
83	62	frnd 6696	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐸)
84	83, 81	sseqtrrd 3973	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐻 ⊆ dom 𝑆)
85	82, 84	unssd 4144	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂 ∪ ran 𝐻) ⊆ dom 𝑆)
86		funimass4 6927	. . . . . . . . . 10 ⊢ ((Fun 𝑆 ∧ (𝑂 ∪ ran 𝐻) ⊆ dom 𝑆) → ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ ∀𝑥 ∈ (𝑂 ∪ ran 𝐻)(𝑆‘𝑥) ∈ (𝐾𝐶𝐵)))
87	76, 85, 86	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ ∀𝑥 ∈ (𝑂 ∪ ran 𝐻)(𝑆‘𝑥) ∈ (𝐾𝐶𝐵)))
88	72, 87	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → (𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵))
89		mclsax.8	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏)
90	89	3exp2 1367	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥𝑀𝑦 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))) → 𝑎𝐾𝑏))))
91	90	imp4b 425	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥𝑀𝑦) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))) → 𝑎𝐾𝑏))
92	91	ralrimivv 3202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥𝑀𝑦) → ∀𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥)))∀𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))𝑎𝐾𝑏)
93		dfss3 3925	. . . . . . . . . . . 12 ⊢ (((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾 ↔ ∀𝑧 ∈ ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦))))𝑧 ∈ 𝐾)
94		eleq1 2849	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 ∈ 𝐾 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝐾))
95		df-br 5100	. . . . . . . . . . . . . 14 ⊢ (𝑎𝐾𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ 𝐾)
96	94, 95	bitr4di 291	. . . . . . . . . . . . 13 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ → (𝑧 ∈ 𝐾 ↔ 𝑎𝐾𝑏))
97	96	ralxp 5811	. . . . . . . . . . . 12 ⊢ (∀𝑧 ∈ ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦))))𝑧 ∈ 𝐾 ↔ ∀𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥)))∀𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))𝑎𝐾𝑏)
98	93, 97	bitri 277	. . . . . . . . . . 11 ⊢ (((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾 ↔ ∀𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥)))∀𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))𝑎𝐾𝑏)
99	92, 98	sylibr 236	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥𝑀𝑦) → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)
100	99	ex 416	. . . . . . . . 9 ⊢ (𝜑 → (𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))
101	100	alrimivv 1947	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))
102	88, 101	jca 519	. . . . . . 7 ⊢ (𝜑 → ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)))
103		imaeq1 6041	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → (𝑠 “ (𝑂 ∪ ran 𝐻)) = (𝑆 “ (𝑂 ∪ ran 𝐻)))
104	103	sseq1d 3967	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → ((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ (𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵)))
105		fveq1 6862	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑆 → (𝑠‘(𝐻‘𝑥)) = (𝑆‘(𝐻‘𝑥)))
106	105	fveq2d 6867	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑆 → (𝑊‘(𝑠‘(𝐻‘𝑥))) = (𝑊‘(𝑆‘(𝐻‘𝑥))))
107		fveq1 6862	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑆 → (𝑠‘(𝐻‘𝑦)) = (𝑆‘(𝐻‘𝑦)))
108	107	fveq2d 6867	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑆 → (𝑊‘(𝑠‘(𝐻‘𝑦))) = (𝑊‘(𝑆‘(𝐻‘𝑦))))
109	106, 108	xpeq12d 5676	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑆 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) = ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))))
110	109	sseq1d 3967	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑆 → (((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾 ↔ ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))
111	110	imbi2d 342	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → ((𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ (𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)))
112	111	2albidv 1942	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)))
113	104, 112	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) ↔ ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))))
114		fveq1 6862	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (𝑠‘𝑃) = (𝑆‘𝑃))
115	114	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → ((𝑠‘𝑃) ∈ 𝑐 ↔ (𝑆‘𝑃) ∈ 𝑐))
116	113, 115	imbi12d 346	. . . . . . . . 9 ⊢ (𝑠 = 𝑆 → ((((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) ↔ (((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑆‘𝑃) ∈ 𝑐)))
117	116	rspcv 3577	. . . . . . . 8 ⊢ (𝑆 ∈ ran 𝐿 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) → (((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑆‘𝑃) ∈ 𝑐)))
118	73, 117	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) → (((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑆‘𝑃) ∈ 𝑐)))
119	102, 118	mpid 44	. . . . . 6 ⊢ (𝜑 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) → (𝑆‘𝑃) ∈ 𝑐))
120	33, 119	embantd 59	. . . . 5 ⊢ (𝜑 → ((⟨𝑀, 𝑂, 𝑃⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)) → (𝑆‘𝑃) ∈ 𝑐))
121	27, 55, 120	3syld 60	. . . 4 ⊢ (𝜑 → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝑆‘𝑃) ∈ 𝑐))
122	121	alrimiv 1946	. . 3 ⊢ (𝜑 → ∀𝑐(((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝑆‘𝑃) ∈ 𝑐))
123		fvex 6876	. . . 4 ⊢ (𝑆‘𝑃) ∈ V
124	123	elintab 4916	. . 3 ⊢ ((𝑆‘𝑃) ∈ ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ↔ ∀𝑐(((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝑆‘𝑃) ∈ 𝑐))
125	122, 124	sylibr 236	. 2 ⊢ (𝜑 → (𝑆‘𝑃) ∈ ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})
126	125, 14	eleqtrrd 2864	1 ⊢ (𝜑 → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1097  ∀wal 1557   = wceq 1559   ∈ wcel 2141  {cab 2739  ∀wral 3075  Vcvv 3453   ∪ cun 3902   ⊆ wss 3904  ⟨cop 4587  ⟨cotp 4589  ∩ cint 4904   class class class wbr 5099   × cxp 5643  ^◡ccnv 5644  dom cdm 5645  ran crn 5646   “ cima 5648  Fun wfun 6511   Fn wfn 6512  ⟶wf 6513  ‘cfv 6517  (class class class)co 7392  Fincfn 8923  mVRcmvar 35775  mAxcmax 35779  mExcmex 35781  mDVcmdv 35782  mVarscmvrs 35783  mSubstcmsub 35785  mVHcmvh 35786  mPreStcmpst 35787  mStatcmsta 35789  mFScmfs 35790  mClscmcls 35791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146  ax-pre-mulgt0 11147

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-ot 4590  df-uni 4865  df-int 4905  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-riota 7349  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7843  df-1st 7966  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-1o 8432  df-er 8673  df-map 8805  df-pm 8806  df-en 8924  df-dom 8925  df-sdom 8926  df-fin 8927  df-card 9894  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11413  df-neg 11414  df-nn 12208  df-2 12277  df-n0 12479  df-z 12566  df-uz 12837  df-fz 13510  df-fzo 13657  df-seq 14012  df-hash 14341  df-word 14524  df-concat 14581  df-s1 14607  df-struct 17166  df-sets 17183  df-slot 17201  df-ndx 17213  df-base 17229  df-ress 17250  df-plusg 17282  df-0g 17453  df-gsum 17454  df-mgm 18657  df-sgrp 18736  df-mnd 18752  df-submnd 18801  df-frmd 18866  df-mrex 35800  df-mex 35801  df-mrsub 35804  df-msub 35805  df-mvh 35806  df-mpst 35807  df-msr 35808  df-msta 35809  df-mfs 35810  df-mcls 35811

This theorem is referenced by:  mclsppslem  35897