mclsval - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mclsval		Structured version Visualization version GIF version

Theorem mclsval 34543

Description: The function mapping variables to variable expressions is one-to-one. (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	⊢ (𝜑 → 𝐵 ⊆ 𝐸)
mclsval.h	⊢ 𝐻 = (mVH‘𝑇)
mclsval.a	⊢ 𝐴 = (mAx‘𝑇)
mclsval.s	⊢ 𝑆 = (mSubst‘𝑇)
mclsval.v	⊢ 𝑉 = (mVars‘𝑇)

**Assertion**
Ref	Expression
mclsval	⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})

Distinct variable groups: 𝑚,𝑐,𝑜,𝑝,𝑠,𝐸 𝑥,𝑐,𝐻,𝑚,𝑜,𝑝,𝑠 𝑦,𝑐,𝐵,𝑚,𝑜,𝑝,𝑠,𝑥 𝐶,𝑚,𝑜,𝑝,𝑠,𝑥 𝐴,𝑐,𝑚,𝑜,𝑝,𝑠 𝑆,𝑐,𝑠,𝑥,𝑦 𝑇,𝑐,𝑚,𝑜,𝑝,𝑠,𝑥,𝑦 𝜑,𝑐,𝑚,𝑜,𝑝,𝑠,𝑥,𝑦 𝑉,𝑐,𝑥 𝐾,𝑐,𝑚,𝑜,𝑝,𝑠,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑥,𝑦) 𝐶(𝑦,𝑐) 𝐷(𝑥,𝑦,𝑚,𝑜,𝑠,𝑝,𝑐) 𝑆(𝑚,𝑜,𝑝) 𝐸(𝑥,𝑦) 𝐻(𝑦) 𝑉(𝑦,𝑚,𝑜,𝑠,𝑝)

Proof of Theorem mclsval Dummy variables ℎ 𝑑 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mclsval.c	. . 3 ⊢ 𝐶 = (mCls‘𝑇)
2		mclsval.1	. . . 4 ⊢ (𝜑 → 𝑇 ∈ mFS)
3		elex 3493	. . . 4 ⊢ (𝑇 ∈ mFS → 𝑇 ∈ V)
4		fveq2 6889	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (mDV‘𝑡) = (mDV‘𝑇))
5		mclsval.d	. . . . . . . 8 ⊢ 𝐷 = (mDV‘𝑇)
6	4, 5	eqtr4di 2791	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (mDV‘𝑡) = 𝐷)
7	6	pweqd 4619	. . . . . 6 ⊢ (𝑡 = 𝑇 → 𝒫 (mDV‘𝑡) = 𝒫 𝐷)
8		fveq2 6889	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇))
9		mclsval.e	. . . . . . . 8 ⊢ 𝐸 = (mEx‘𝑇)
10	8, 9	eqtr4di 2791	. . . . . . 7 ⊢ (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸)
11	10	pweqd 4619	. . . . . 6 ⊢ (𝑡 = 𝑇 → 𝒫 (mEx‘𝑡) = 𝒫 𝐸)
12		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (mVH‘𝑡) = (mVH‘𝑇))
13		mclsval.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (mVH‘𝑇)
14	12, 13	eqtr4di 2791	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (mVH‘𝑡) = 𝐻)
15	14	rneqd 5936	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ran (mVH‘𝑡) = ran 𝐻)
16	15	uneq2d 4163	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (ℎ ∪ ran (mVH‘𝑡)) = (ℎ ∪ ran 𝐻))
17	16	sseq1d 4013	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ↔ (ℎ ∪ ran 𝐻) ⊆ 𝑐))
18		fveq2 6889	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (mAx‘𝑡) = (mAx‘𝑇))
19		mclsval.a	. . . . . . . . . . . . . 14 ⊢ 𝐴 = (mAx‘𝑇)
20	18, 19	eqtr4di 2791	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → (mAx‘𝑡) = 𝐴)
21	20	eleq2d 2820	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) ↔ ⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴))
22		fveq2 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → (mSubst‘𝑡) = (mSubst‘𝑇))
23		mclsval.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (mSubst‘𝑇)
24	22, 23	eqtr4di 2791	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (mSubst‘𝑡) = 𝑆)
25	24	rneqd 5936	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ran (mSubst‘𝑡) = ran 𝑆)
26	15	uneq2d 4163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → (𝑜 ∪ ran (mVH‘𝑡)) = (𝑜 ∪ ran 𝐻))
27	26	imaeq2d 6058	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) = (𝑠 “ (𝑜 ∪ ran 𝐻)))
28	27	sseq1d 4013	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → ((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ↔ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐))
29		fveq2 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇))
30		mclsval.v	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑉 = (mVars‘𝑇)
31	29, 30	eqtr4di 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉)
32	14	fveq1d 6891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → ((mVH‘𝑡)‘𝑥) = (𝐻‘𝑥))
33	32	fveq2d 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → (𝑠‘((mVH‘𝑡)‘𝑥)) = (𝑠‘(𝐻‘𝑥)))
34	31, 33	fveq12d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) = (𝑉‘(𝑠‘(𝐻‘𝑥))))
35	14	fveq1d 6891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 = 𝑇 → ((mVH‘𝑡)‘𝑦) = (𝐻‘𝑦))
36	35	fveq2d 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑇 → (𝑠‘((mVH‘𝑡)‘𝑦)) = (𝑠‘(𝐻‘𝑦)))
37	31, 36	fveq12d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑇 → ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))) = (𝑉‘(𝑠‘(𝐻‘𝑦))))
38	34, 37	xpeq12d 5707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑇 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) = ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))))
39	38	sseq1d 4013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑇 → ((((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑 ↔ ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑))
40	39	imbi2d 341	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑇 → ((𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) ↔ (𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)))
41	40	2albidv 1927	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑇 → (∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) ↔ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)))
42	28, 41	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑇 → (((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑))))
43	42	imbi1d 342	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑇 → ((((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))
44	25, 43	raleqbidv 3343	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑇 → (∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))
45	21, 44	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑇 → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))))
46	45	albidv 1924	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))))
47	46	2albidv 1927	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → (∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))))
48	17, 47	anbi12d 632	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))) ↔ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))))
49	48	abbidv 2802	. . . . . . 7 ⊢ (𝑡 = 𝑇 → {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))} = {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))})
50	49	inteqd 4955	. . . . . 6 ⊢ (𝑡 = 𝑇 → ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))} = ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))})
51	7, 11, 50	mpoeq123dv 7481	. . . . 5 ⊢ (𝑡 = 𝑇 → (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}) = (𝑑 ∈ 𝒫 𝐷, ℎ ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
52		df-mcls 34477	. . . . 5 ⊢ mCls = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
53	5	fvexi 6903	. . . . . . 7 ⊢ 𝐷 ∈ V
54	53	pwex 5378	. . . . . 6 ⊢ 𝒫 𝐷 ∈ V
55	9	fvexi 6903	. . . . . . 7 ⊢ 𝐸 ∈ V
56	55	pwex 5378	. . . . . 6 ⊢ 𝒫 𝐸 ∈ V
57	54, 56	mpoex 8063	. . . . 5 ⊢ (𝑑 ∈ 𝒫 𝐷, ℎ ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}) ∈ V
58	51, 52, 57	fvmpt 6996	. . . 4 ⊢ (𝑇 ∈ V → (mCls‘𝑇) = (𝑑 ∈ 𝒫 𝐷, ℎ ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
59	2, 3, 58	3syl 18	. . 3 ⊢ (𝜑 → (mCls‘𝑇) = (𝑑 ∈ 𝒫 𝐷, ℎ ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
60	1, 59	eqtrid 2785	. 2 ⊢ (𝜑 → 𝐶 = (𝑑 ∈ 𝒫 𝐷, ℎ ∈ 𝒫 𝐸 ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
61		simprr 772	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → ℎ = 𝐵)
62	61	uneq1d 4162	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (ℎ ∪ ran 𝐻) = (𝐵 ∪ ran 𝐻))
63	62	sseq1d 4013	. . . . 5 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ↔ (𝐵 ∪ ran 𝐻) ⊆ 𝑐))
64		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → 𝑑 = 𝐾)
65	64	sseq2d 4014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑 ↔ ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾))
66	65	imbi2d 341	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → ((𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑) ↔ (𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))
67	66	2albidv 1927	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑) ↔ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))
68	67	anbi2d 630	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾))))
69	68	imbi1d 342	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))
70	69	ralbidv 3178	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))
71	70	imbi2d 341	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
72	71	albidv 1924	. . . . . 6 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
73	72	2albidv 1927	. . . . 5 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))))
74	63, 73	anbi12d 632	. . . 4 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → (((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))) ↔ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))))
75	74	abbidv 2802	. . 3 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))} = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})
76	75	inteqd 4955	. 2 ⊢ ((𝜑 ∧ (𝑑 = 𝐾 ∧ ℎ = 𝐵)) → ∩ {𝑐 ∣ ((ℎ ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))} = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})
77		mclsval.2	. . 3 ⊢ (𝜑 → 𝐾 ⊆ 𝐷)
78	53	elpw2 5345	. . 3 ⊢ (𝐾 ∈ 𝒫 𝐷 ↔ 𝐾 ⊆ 𝐷)
79	77, 78	sylibr 233	. 2 ⊢ (𝜑 → 𝐾 ∈ 𝒫 𝐷)
80		mclsval.3	. . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐸)
81	55	elpw2 5345	. . 3 ⊢ (𝐵 ∈ 𝒫 𝐸 ↔ 𝐵 ⊆ 𝐸)
82	80, 81	sylibr 233	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐸)
83	5, 9, 1, 2, 77, 80, 13, 19, 23, 30	mclsssvlem 34542	. . 3 ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸)
84	55	ssex 5321	. . 3 ⊢ (∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝐸 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ∈ V)
85	83, 84	syl 17	. 2 ⊢ (𝜑 → ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ∈ V)
86	60, 76, 79, 82, 85	ovmpod 7557	1 ⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻‘𝑥))) × (𝑉‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∀wal 1540 = wceq 1542 ∈ wcel 2107 {cab 2710 ∀wral 3062 Vcvv 3475 ∪ cun 3946 ⊆ wss 3948 𝒫 cpw 4602 ⟨cotp 4636 ∩ cint 4950 class class class wbr 5148 × cxp 5674 ran crn 5677 “ cima 5679 ‘cfv 6541 (class class class)co 7406 ∈ cmpo 7408 mAxcmax 34445 mExcmex 34447 mDVcmdv 34448 mVarscmvrs 34449 mSubstcmsub 34451 mVHcmvh 34452 mFScmfs 34456 mClscmcls 34457

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-ot 4637 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-er 8700 df-map 8819 df-pm 8820 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-2 12272 df-n0 12470 df-z 12556 df-uz 12820 df-fz 13482 df-fzo 13625 df-seq 13964 df-hash 14288 df-word 14462 df-concat 14518 df-s1 14543 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-0g 17384 df-gsum 17385 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-frmd 18727 df-mrex 34466 df-mex 34467 df-mrsub 34470 df-msub 34471 df-mvh 34472 df-mpst 34473 df-msr 34474 df-msta 34475 df-mfs 34476 df-mcls 34477

This theorem is referenced by: mclsssv 34544 ssmclslem 34545 ss2mcls 34548 mclsax 34549 mclsind 34550

W3C validator