Theorem msubco 30217

Description: The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)

Hypothesis

Ref	Expression
msubco.s	|- S = (mSubst ` T )

Assertion

Ref	Expression
msubco	|- ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )

Proof of Theorem msubco

Dummy variables f g h x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2461	. . . . 5 |- (mEx ` T ) = (mEx ` T )
2		eqid 2461	. . . . 5 |- (mRSubst ` T ) = (mRSubst ` T )
3		msubco.s	. . . . 5 |- S = (mSubst ` T )
4	1, 2, 3	elmsubrn 30214	. . . 4 |- ran S = ran ( f e. ran (mRSubst ` T ) |-> ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
5	4	eleq2i 2531	. . 3 |- ( F e. ran S <-> F e. ran ( f e. ran (mRSubst ` T ) |-> ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) ) )
6		eqid 2461	. . . 4 |- ( f e. ran (mRSubst ` T ) |-> ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) ) = ( f e. ran (mRSubst ` T ) |-> ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
7		fvex 5897	. . . . 5 |- (mEx ` T ) e. _V
8	7	mptex 6160	. . . 4 |- ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) e. _V
9	6, 8	elrnmpti 5103	. . 3 |- ( F e. ran ( f e. ran (mRSubst ` T ) |-> ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) ) <-> E. f e. ran (mRSubst ` T ) F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
10	5, 9	bitri 257	. 2 |- ( F e. ran S <-> E. f e. ran (mRSubst ` T ) F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
11	1, 2, 3	elmsubrn 30214	. . . 4 |- ran S = ran ( g e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
12	11	eleq2i 2531	. . 3 |- ( G e. ran S <-> G e. ran ( g e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
13		eqid 2461	. . . 4 |- ( g e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) = ( g e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
14	7	mptex 6160	. . . 4 |- ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) e. _V
15	13, 14	elrnmpti 5103	. . 3 |- ( G e. ran ( g e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) <-> E. g e. ran (mRSubst ` T ) G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
16	12, 15	bitri 257	. 2 |- ( G e. ran S <-> E. g e. ran (mRSubst ` T ) G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
17		reeanv 2969	. . 3 |- ( E. f e. ran (mRSubst ` T ) E. g e. ran (mRSubst ` T ) ( F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) <-> ( E. f e. ran (mRSubst ` T ) F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ E. g e. ran (mRSubst ` T ) G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
18		simpr 467	. . . . . . . . . . . 12 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> y e. (mEx ` T ) )
19		eqid 2461	. . . . . . . . . . . . 13 |- (mTC ` T ) = (mTC ` T )
20		eqid 2461	. . . . . . . . . . . . 13 |- (mREx ` T ) = (mREx ` T )
21	19, 1, 20	mexval 30188	. . . . . . . . . . . 12 |- (mEx ` T ) = ( (mTC ` T ) X. (mREx ` T ) )
22	18, 21	syl6eleq 2549	. . . . . . . . . . 11 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> y e. ( (mTC ` T ) X. (mREx ` T ) ) )
23		xp1st 6849	. . . . . . . . . . 11 |- ( y e. ( (mTC ` T ) X. (mREx ` T ) ) -> ( 1st ` y ) e. (mTC ` T ) )
24	22, 23	syl 17	. . . . . . . . . 10 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> ( 1st ` y ) e. (mTC ` T ) )
25	2, 20	mrsubf 30203	. . . . . . . . . . . 12 |- ( g e. ran (mRSubst ` T ) -> g : (mREx ` T ) --> (mREx ` T ) )
26	25	ad2antlr 738	. . . . . . . . . . 11 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> g : (mREx ` T ) --> (mREx ` T ) )
27		xp2nd 6850	. . . . . . . . . . . 12 |- ( y e. ( (mTC ` T ) X. (mREx ` T ) ) -> ( 2nd ` y ) e. (mREx ` T ) )
28	22, 27	syl 17	. . . . . . . . . . 11 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> ( 2nd ` y ) e. (mREx ` T ) )
29	26, 28	ffvelrnd 6045	. . . . . . . . . 10 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> ( g ` ( 2nd ` y ) ) e. (mREx ` T ) )
30		opelxpi 4884	. . . . . . . . . 10 |- ( ( ( 1st ` y ) e. (mTC ` T ) /\ ( g ` ( 2nd ` y ) ) e. (mREx ` T ) ) -> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. e. ( (mTC ` T ) X. (mREx ` T ) ) )
31	24, 29, 30	syl2anc 671	. . . . . . . . 9 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. e. ( (mTC ` T ) X. (mREx ` T ) ) )
32	31, 21	syl6eleqr 2550	. . . . . . . 8 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. e. (mEx ` T ) )
33		eqidd 2462	. . . . . . . 8 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
34		eqidd 2462	. . . . . . . 8 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
35		fvex 5897	. . . . . . . . . 10 |- ( 1st ` y ) e. _V
36		fvex 5897	. . . . . . . . . 10 |- ( g ` ( 2nd ` y ) ) e. _V
37	35, 36	op1std 6829	. . . . . . . . 9 |- ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> ( 1st ` x ) = ( 1st ` y ) )
38	35, 36	op2ndd 6830	. . . . . . . . . 10 |- ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> ( 2nd ` x ) = ( g ` ( 2nd ` y ) ) )
39	38	fveq2d 5891	. . . . . . . . 9 |- ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> ( f ` ( 2nd ` x ) ) = ( f ` ( g ` ( 2nd ` y ) ) ) )
40	37, 39	opeq12d 4187	. . . . . . . 8 |- ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. = <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. )
41	32, 33, 34, 40	fmptco 6079	. . . . . . 7 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. ) )
42		fvco3 5964	. . . . . . . . . 10 |- ( ( g : (mREx ` T ) --> (mREx ` T ) /\ ( 2nd ` y ) e. (mREx ` T ) ) -> ( ( f o. g ) ` ( 2nd ` y ) ) = ( f ` ( g ` ( 2nd ` y ) ) ) )
43	26, 28, 42	syl2anc 671	. . . . . . . . 9 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> ( ( f o. g ) ` ( 2nd ` y ) ) = ( f ` ( g ` ( 2nd ` y ) ) ) )
44	43	opeq2d 4186	. . . . . . . 8 |- ( ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) /\ y e. (mEx ` T ) ) -> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. = <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. )
45	44	mpteq2dva 4502	. . . . . . 7 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. ) )
46	41, 45	eqtr4d 2498	. . . . . 6 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) )
47	2	mrsubco 30207	. . . . . . . 8 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( f o. g ) e. ran (mRSubst ` T ) )
48	7	mptex 6160	. . . . . . . 8 |- ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. _V
49		eqid 2461	. . . . . . . . 9 |- ( h e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) ) = ( h e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) )
50		fveq1 5886	. . . . . . . . . . 11 |- ( h = ( f o. g ) -> ( h ` ( 2nd ` y ) ) = ( ( f o. g ) ` ( 2nd ` y ) ) )
51	50	opeq2d 4186	. . . . . . . . . 10 |- ( h = ( f o. g ) -> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. = <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. )
52	51	mpteq2dv 4503	. . . . . . . . 9 |- ( h = ( f o. g ) -> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) )
53	49, 52	elrnmpt1s 5100	. . . . . . . 8 |- ( ( ( f o. g ) e. ran (mRSubst ` T ) /\ ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. _V ) -> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. ran ( h e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) ) )
54	47, 48, 53	sylancl 673	. . . . . . 7 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. ran ( h e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) ) )
55	1, 2, 3	elmsubrn 30214	. . . . . . 7 |- ran S = ran ( h e. ran (mRSubst ` T ) |-> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) )
56	54, 55	syl6eleqr 2550	. . . . . 6 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. ran S )
57	46, 56	eqeltrd 2539	. . . . 5 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) e. ran S )
58		coeq1 5010	. . . . . . 7 |- ( F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) -> ( F o. G ) = ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. G ) )
59		coeq2 5011	. . . . . . 7 |- ( G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) -> ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. G ) = ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
60	58, 59	sylan9eq 2515	. . . . . 6 |- ( ( F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) = ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
61	60	eleq1d 2523	. . . . 5 |- ( ( F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( ( F o. G ) e. ran S <-> ( ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) e. ran S ) )
62	57, 61	syl5ibrcom 230	. . . 4 |- ( ( f e. ran (mRSubst ` T ) /\ g e. ran (mRSubst ` T ) ) -> ( ( F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) e. ran S ) )
63	62	rexlimivv 2895	. . 3 |- ( E. f e. ran (mRSubst ` T ) E. g e. ran (mRSubst ` T ) ( F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) e. ran S )
64	17, 63	sylbir 218	. 2 |- ( ( E. f e. ran (mRSubst ` T ) F = ( x e. (mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ E. g e. ran (mRSubst ` T ) G = ( y e. (mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) e. ran S )
65	10, 16, 64	syl2anb 486	1 |- ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1454   e. wcel 1897   E.wrex 2749   _Vcvv 3056   <.cop 3985   |-> cmpt 4474   X. cxp 4850   ran crn 4853   o. ccom 4856   -->wf 5596   ` cfv 5600   1stc1st 6817   2ndc2nd 6818  mTCcmtc 30150  mRExcmrex 30152  mExcmex 30153  mRSubstcmrsub 30156  mSubstcmsub 30157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-map 7499  df-pm 7500  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-2 10695  df-n0 10898  df-z 10966  df-uz 11188  df-fz 11813  df-fzo 11946  df-seq 12245  df-hash 12547  df-word 12696  df-lsw 12697  df-concat 12698  df-s1 12699  df-substr 12700  df-struct 15171  df-ndx 15172  df-slot 15173  df-base 15174  df-sets 15175  df-ress 15176  df-plusg 15251  df-0g 15388  df-gsum 15389  df-mgm 16536  df-sgrp 16575  df-mnd 16585  df-mhm 16630  df-submnd 16631  df-frmd 16681  df-vrmd 16682  df-mrex 30172  df-mex 30173  df-mrsub 30176  df-msub 30177

This theorem is referenced by:  mclsppslem  30269