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

Theorem mclsval 35167
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.
StepHypRef Expression
1 mclsval.c . . 3 𝐶 = (mCls‘𝑇)
2 mclsval.1 . . . 4 (𝜑𝑇 ∈ mFS)
3 elex 3489 . . . 4 (𝑇 ∈ mFS → 𝑇 ∈ V)
4 fveq2 6891 . . . . . . . 8 (𝑡 = 𝑇 → (mDV‘𝑡) = (mDV‘𝑇))
5 mclsval.d . . . . . . . 8 𝐷 = (mDV‘𝑇)
64, 5eqtr4di 2786 . . . . . . 7 (𝑡 = 𝑇 → (mDV‘𝑡) = 𝐷)
76pweqd 4615 . . . . . 6 (𝑡 = 𝑇 → 𝒫 (mDV‘𝑡) = 𝒫 𝐷)
8 fveq2 6891 . . . . . . . 8 (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇))
9 mclsval.e . . . . . . . 8 𝐸 = (mEx‘𝑇)
108, 9eqtr4di 2786 . . . . . . 7 (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸)
1110pweqd 4615 . . . . . 6 (𝑡 = 𝑇 → 𝒫 (mEx‘𝑡) = 𝒫 𝐸)
12 fveq2 6891 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (mVH‘𝑡) = (mVH‘𝑇))
13 mclsval.h . . . . . . . . . . . . 13 𝐻 = (mVH‘𝑇)
1412, 13eqtr4di 2786 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (mVH‘𝑡) = 𝐻)
1514rneqd 5934 . . . . . . . . . . 11 (𝑡 = 𝑇 → ran (mVH‘𝑡) = ran 𝐻)
1615uneq2d 4159 . . . . . . . . . 10 (𝑡 = 𝑇 → ( ∪ ran (mVH‘𝑡)) = ( ∪ ran 𝐻))
1716sseq1d 4009 . . . . . . . . 9 (𝑡 = 𝑇 → (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ↔ ( ∪ ran 𝐻) ⊆ 𝑐))
18 fveq2 6891 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (mAx‘𝑡) = (mAx‘𝑇))
19 mclsval.a . . . . . . . . . . . . . 14 𝐴 = (mAx‘𝑇)
2018, 19eqtr4di 2786 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (mAx‘𝑡) = 𝐴)
2120eleq2d 2815 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) ↔ ⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴))
22 fveq2 6891 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇 → (mSubst‘𝑡) = (mSubst‘𝑇))
23 mclsval.s . . . . . . . . . . . . . . 15 𝑆 = (mSubst‘𝑇)
2422, 23eqtr4di 2786 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (mSubst‘𝑡) = 𝑆)
2524rneqd 5934 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ran (mSubst‘𝑡) = ran 𝑆)
2615uneq2d 4159 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → (𝑜 ∪ ran (mVH‘𝑡)) = (𝑜 ∪ ran 𝐻))
2726imaeq2d 6057 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) = (𝑠 “ (𝑜 ∪ ran 𝐻)))
2827sseq1d 4009 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇 → ((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ↔ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐))
29 fveq2 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇))
30 mclsval.v . . . . . . . . . . . . . . . . . . . . 21 𝑉 = (mVars‘𝑇)
3129, 30eqtr4di 2786 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉)
3214fveq1d 6893 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → ((mVH‘𝑡)‘𝑥) = (𝐻𝑥))
3332fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (𝑠‘((mVH‘𝑡)‘𝑥)) = (𝑠‘(𝐻𝑥)))
3431, 33fveq12d 6898 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) = (𝑉‘(𝑠‘(𝐻𝑥))))
3514fveq1d 6893 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → ((mVH‘𝑡)‘𝑦) = (𝐻𝑦))
3635fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (𝑠‘((mVH‘𝑡)‘𝑦)) = (𝑠‘(𝐻𝑦)))
3731, 36fveq12d 6898 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))) = (𝑉‘(𝑠‘(𝐻𝑦))))
3834, 37xpeq12d 5703 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) = ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))))
3938sseq1d 4009 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑 ↔ ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑))
4039imbi2d 340 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → ((𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) ↔ (𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)))
41402albidv 1919 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇 → (∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) ↔ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)))
4228, 41anbi12d 631 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑))))
4342imbi1d 341 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ((((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))
4425, 43raleqbidv 3338 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))
4521, 44imbi12d 344 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))))
4645albidv 1916 . . . . . . . . . 10 (𝑡 = 𝑇 → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))))
47462albidv 1919 . . . . . . . . 9 (𝑡 = 𝑇 → (∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))))
4817, 47anbi12d 631 . . . . . . . 8 (𝑡 = 𝑇 → ((( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))) ↔ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))))
4948abbidv 2797 . . . . . . 7 (𝑡 = 𝑇 → {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))})
5049inteqd 4949 . . . . . 6 (𝑡 = 𝑇 {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))})
517, 11, 50mpoeq123dv 7489 . . . . 5 (𝑡 = 𝑇 → (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}) = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
52 df-mcls 35101 . . . . 5 mCls = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
535fvexi 6905 . . . . . . 7 𝐷 ∈ V
5453pwex 5374 . . . . . 6 𝒫 𝐷 ∈ V
559fvexi 6905 . . . . . . 7 𝐸 ∈ V
5655pwex 5374 . . . . . 6 𝒫 𝐸 ∈ V
5754, 56mpoex 8078 . . . . 5 (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}) ∈ V
5851, 52, 57fvmpt 6999 . . . 4 (𝑇 ∈ V → (mCls‘𝑇) = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
592, 3, 583syl 18 . . 3 (𝜑 → (mCls‘𝑇) = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
601, 59eqtrid 2780 . 2 (𝜑𝐶 = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
61 simprr 772 . . . . . . 7 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → = 𝐵)
6261uneq1d 4158 . . . . . 6 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ( ∪ ran 𝐻) = (𝐵 ∪ ran 𝐻))
6362sseq1d 4009 . . . . 5 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (( ∪ ran 𝐻) ⊆ 𝑐 ↔ (𝐵 ∪ ran 𝐻) ⊆ 𝑐))
64 simprl 770 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → 𝑑 = 𝐾)
6564sseq2d 4010 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑 ↔ ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾))
6665imbi2d 340 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑) ↔ (𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)))
67662albidv 1919 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑) ↔ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)))
6867anbi2d 629 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾))))
6968imbi1d 341 . . . . . . . . 9 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))
7069ralbidv 3173 . . . . . . . 8 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))
7170imbi2d 340 . . . . . . 7 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐))))
7271albidv 1916 . . . . . 6 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐))))
73722albidv 1919 . . . . 5 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐))))
7463, 73anbi12d 631 . . . 4 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))) ↔ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))))
7574abbidv 2797 . . 3 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))})
7675inteqd 4949 . 2 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))})
77 mclsval.2 . . 3 (𝜑𝐾𝐷)
7853elpw2 5341 . . 3 (𝐾 ∈ 𝒫 𝐷𝐾𝐷)
7977, 78sylibr 233 . 2 (𝜑𝐾 ∈ 𝒫 𝐷)
80 mclsval.3 . . 3 (𝜑𝐵𝐸)
8155elpw2 5341 . . 3 (𝐵 ∈ 𝒫 𝐸𝐵𝐸)
8280, 81sylibr 233 . 2 (𝜑𝐵 ∈ 𝒫 𝐸)
835, 9, 1, 2, 77, 80, 13, 19, 23, 30mclsssvlem 35166 . . 3 (𝜑 {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ⊆ 𝐸)
8455ssex 5315 . . 3 ( {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ⊆ 𝐸 {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ∈ V)
8583, 84syl 17 . 2 (𝜑 {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ∈ V)
8660, 76, 79, 82, 85ovmpod 7567 1 (𝜑 → (𝐾𝐶𝐵) = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1532   = wceq 1534  wcel 2099  {cab 2705  wral 3057  Vcvv 3470  cun 3943  wss 3945  𝒫 cpw 4598  cotp 4632   cint 4944   class class class wbr 5142   × cxp 5670  ran crn 5673  cima 5675  cfv 6542  (class class class)co 7414  cmpo 7416  mAxcmax 35069  mExcmex 35071  mDVcmdv 35072  mVarscmvrs 35073  mSubstcmsub 35075  mVHcmvh 35076  mFScmfs 35080  mClscmcls 35081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-ot 4633  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8840  df-pm 8841  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-card 9956  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-nn 12237  df-2 12299  df-n0 12497  df-z 12583  df-uz 12847  df-fz 13511  df-fzo 13654  df-seq 13993  df-hash 14316  df-word 14491  df-concat 14547  df-s1 14572  df-struct 17109  df-sets 17126  df-slot 17144  df-ndx 17156  df-base 17174  df-ress 17203  df-plusg 17239  df-0g 17416  df-gsum 17417  df-mgm 18593  df-sgrp 18672  df-mnd 18688  df-submnd 18734  df-frmd 18794  df-mrex 35090  df-mex 35091  df-mrsub 35094  df-msub 35095  df-mvh 35096  df-mpst 35097  df-msr 35098  df-msta 35099  df-mfs 35100  df-mcls 35101
This theorem is referenced by:  mclsssv  35168  ssmclslem  35169  ss2mcls  35172  mclsax  35173  mclsind  35174
  Copyright terms: Public domain W3C validator