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

Theorem mclsval 31165
 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 3198 . . . 4 (𝑇 ∈ mFS → 𝑇 ∈ V)
4 fveq2 6148 . . . . . . . 8 (𝑡 = 𝑇 → (mDV‘𝑡) = (mDV‘𝑇))
5 mclsval.d . . . . . . . 8 𝐷 = (mDV‘𝑇)
64, 5syl6eqr 2673 . . . . . . 7 (𝑡 = 𝑇 → (mDV‘𝑡) = 𝐷)
76pweqd 4135 . . . . . 6 (𝑡 = 𝑇 → 𝒫 (mDV‘𝑡) = 𝒫 𝐷)
8 fveq2 6148 . . . . . . . 8 (𝑡 = 𝑇 → (mEx‘𝑡) = (mEx‘𝑇))
9 mclsval.e . . . . . . . 8 𝐸 = (mEx‘𝑇)
108, 9syl6eqr 2673 . . . . . . 7 (𝑡 = 𝑇 → (mEx‘𝑡) = 𝐸)
1110pweqd 4135 . . . . . 6 (𝑡 = 𝑇 → 𝒫 (mEx‘𝑡) = 𝒫 𝐸)
12 fveq2 6148 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (mVH‘𝑡) = (mVH‘𝑇))
13 mclsval.h . . . . . . . . . . . . 13 𝐻 = (mVH‘𝑇)
1412, 13syl6eqr 2673 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (mVH‘𝑡) = 𝐻)
1514rneqd 5313 . . . . . . . . . . 11 (𝑡 = 𝑇 → ran (mVH‘𝑡) = ran 𝐻)
1615uneq2d 3745 . . . . . . . . . 10 (𝑡 = 𝑇 → ( ∪ ran (mVH‘𝑡)) = ( ∪ ran 𝐻))
1716sseq1d 3611 . . . . . . . . 9 (𝑡 = 𝑇 → (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ↔ ( ∪ ran 𝐻) ⊆ 𝑐))
18 fveq2 6148 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (mAx‘𝑡) = (mAx‘𝑇))
19 mclsval.a . . . . . . . . . . . . . 14 𝐴 = (mAx‘𝑇)
2018, 19syl6eqr 2673 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (mAx‘𝑡) = 𝐴)
2120eleq2d 2684 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) ↔ ⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴))
22 fveq2 6148 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇 → (mSubst‘𝑡) = (mSubst‘𝑇))
23 mclsval.s . . . . . . . . . . . . . . 15 𝑆 = (mSubst‘𝑇)
2422, 23syl6eqr 2673 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (mSubst‘𝑡) = 𝑆)
2524rneqd 5313 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ran (mSubst‘𝑡) = ran 𝑆)
2615uneq2d 3745 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → (𝑜 ∪ ran (mVH‘𝑡)) = (𝑜 ∪ ran 𝐻))
2726imaeq2d 5425 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) = (𝑠 “ (𝑜 ∪ ran 𝐻)))
2827sseq1d 3611 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇 → ((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ↔ (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐))
29 fveq2 6148 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (mVars‘𝑡) = (mVars‘𝑇))
30 mclsval.v . . . . . . . . . . . . . . . . . . . . 21 𝑉 = (mVars‘𝑇)
3129, 30syl6eqr 2673 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (mVars‘𝑡) = 𝑉)
3214fveq1d 6150 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → ((mVH‘𝑡)‘𝑥) = (𝐻𝑥))
3332fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (𝑠‘((mVH‘𝑡)‘𝑥)) = (𝑠‘(𝐻𝑥)))
3431, 33fveq12d 6154 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) = (𝑉‘(𝑠‘(𝐻𝑥))))
3514fveq1d 6150 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → ((mVH‘𝑡)‘𝑦) = (𝐻𝑦))
3635fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (𝑠‘((mVH‘𝑡)‘𝑦)) = (𝑠‘(𝐻𝑦)))
3731, 36fveq12d 6154 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))) = (𝑉‘(𝑠‘(𝐻𝑦))))
3834, 37xpeq12d 5100 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) = ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))))
3938sseq1d 3611 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑 ↔ ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑))
4039imbi2d 330 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → ((𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) ↔ (𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)))
41402albidv 1848 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇 → (∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑) ↔ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)))
4228, 41anbi12d 746 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑))))
4342imbi1d 331 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → ((((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))
4425, 43raleqbidv 3141 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))
4521, 44imbi12d 334 . . . . . . . . . . 11 (𝑡 = 𝑇 → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))))
4645albidv 1846 . . . . . . . . . 10 (𝑡 = 𝑇 → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))))
47462albidv 1848 . . . . . . . . 9 (𝑡 = 𝑇 → (∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))))
4817, 47anbi12d 746 . . . . . . . 8 (𝑡 = 𝑇 → ((( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))) ↔ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))))
4948abbidv 2738 . . . . . . 7 (𝑡 = 𝑇 → {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))})
5049inteqd 4445 . . . . . 6 (𝑡 = 𝑇 {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))})
517, 11, 50mpt2eq123dv 6670 . . . . 5 (𝑡 = 𝑇 → (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}) = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
52 df-mcls 31099 . . . . 5 mCls = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
53 fvex 6158 . . . . . . . 8 (mDV‘𝑇) ∈ V
545, 53eqeltri 2694 . . . . . . 7 𝐷 ∈ V
5554pwex 4808 . . . . . 6 𝒫 𝐷 ∈ V
56 fvex 6158 . . . . . . . 8 (mEx‘𝑇) ∈ V
579, 56eqeltri 2694 . . . . . . 7 𝐸 ∈ V
5857pwex 4808 . . . . . 6 𝒫 𝐸 ∈ V
5955, 58mpt2ex 7192 . . . . 5 (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}) ∈ V
6051, 52, 59fvmpt 6239 . . . 4 (𝑇 ∈ V → (mCls‘𝑇) = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
612, 3, 603syl 18 . . 3 (𝜑 → (mCls‘𝑇) = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
621, 61syl5eq 2667 . 2 (𝜑𝐶 = (𝑑 ∈ 𝒫 𝐷, ∈ 𝒫 𝐸 {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
63 simprr 795 . . . . . . 7 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → = 𝐵)
6463uneq1d 3744 . . . . . 6 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ( ∪ ran 𝐻) = (𝐵 ∪ ran 𝐻))
6564sseq1d 3611 . . . . 5 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (( ∪ ran 𝐻) ⊆ 𝑐 ↔ (𝐵 ∪ ran 𝐻) ⊆ 𝑐))
66 simprl 793 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → 𝑑 = 𝐾)
6766sseq2d 3612 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑 ↔ ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾))
6867imbi2d 330 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑) ↔ (𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)))
69682albidv 1848 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑) ↔ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)))
7069anbi2d 739 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) ↔ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾))))
7170imbi1d 331 . . . . . . . . 9 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))
7271ralbidv 2980 . . . . . . . 8 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))
7372imbi2d 330 . . . . . . 7 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ (⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐))))
7473albidv 1846 . . . . . 6 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐))))
75742albidv 1848 . . . . 5 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → (∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)) ↔ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐))))
7665, 75anbi12d 746 . . . 4 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → ((( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))) ↔ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))))
7776abbidv 2738 . . 3 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))})
7877inteqd 4445 . 2 ((𝜑 ∧ (𝑑 = 𝐾 = 𝐵)) → {𝑐 ∣ (( ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))} = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))})
79 mclsval.2 . . 3 (𝜑𝐾𝐷)
8054elpw2 4788 . . 3 (𝐾 ∈ 𝒫 𝐷𝐾𝐷)
8179, 80sylibr 224 . 2 (𝜑𝐾 ∈ 𝒫 𝐷)
82 mclsval.3 . . 3 (𝜑𝐵𝐸)
8357elpw2 4788 . . 3 (𝐵 ∈ 𝒫 𝐸𝐵𝐸)
8482, 83sylibr 224 . 2 (𝜑𝐵 ∈ 𝒫 𝐸)
855, 9, 1, 2, 79, 82, 13, 19, 23, 30mclsssvlem 31164 . . 3 (𝜑 {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ⊆ 𝐸)
8657ssex 4762 . . 3 ( {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ⊆ 𝐸 {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ∈ V)
8785, 86syl 17 . 2 (𝜑 {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))} ∈ V)
8862, 78, 81, 84, 87ovmpt2d 6741 1 (𝜑 → (𝐾𝐶𝐵) = {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ 𝐴 → ∀𝑠 ∈ ran 𝑆(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → ((𝑉‘(𝑠‘(𝐻𝑥))) × (𝑉‘(𝑠‘(𝐻𝑦)))) ⊆ 𝐾)) → (𝑠𝑝) ∈ 𝑐)))})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384  ∀wal 1478   = wceq 1480   ∈ wcel 1987  {cab 2607  ∀wral 2907  Vcvv 3186   ∪ cun 3553   ⊆ wss 3555  𝒫 cpw 4130  ⟨cotp 4156  ∩ cint 4440   class class class wbr 4613   × cxp 5072  ran crn 5075   “ cima 5077  ‘cfv 5847  (class class class)co 6604   ↦ cmpt2 6606  mAxcmax 31067  mExcmex 31069  mDVcmdv 31070  mVarscmvrs 31071  mSubstcmsub 31073  mVHcmvh 31074  mFScmfs 31078  mClscmcls 31079 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-ot 4157  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-seq 12742  df-hash 13058  df-word 13238  df-concat 13240  df-s1 13241  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-0g 16023  df-gsum 16024  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-frmd 17307  df-mrex 31088  df-mex 31089  df-mrsub 31092  df-msub 31093  df-mvh 31094  df-mpst 31095  df-msr 31096  df-msta 31097  df-mfs 31098  df-mcls 31099 This theorem is referenced by:  mclsssv  31166  ssmclslem  31167  ss2mcls  31170  mclsax  31171  mclsind  31172
 Copyright terms: Public domain W3C validator