Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mrsubco Structured version   Unicode version

Theorem mrsubco 30106
 Description: The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypothesis
Ref Expression
mrsubco.s mRSubst
Assertion
Ref Expression
mrsubco

Proof of Theorem mrsubco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mrsubco.s . . . . 5 mRSubst
2 eqid 2423 . . . . 5 mREx mREx
31, 2mrsubf 30102 . . . 4 mRExmREx
43adantr 466 . . 3 mRExmREx
51, 2mrsubf 30102 . . . 4 mRExmREx
65adantl 467 . . 3 mRExmREx
7 fco 5694 . . 3 mRExmREx mRExmREx mRExmREx
84, 6, 7syl2anc 665 . 2 mRExmREx
96adantr 466 . . . . 5 mCN mVR mRExmREx
10 eldifi 3525 . . . . . . . . 9 mCN mVR mCN
11 elun1 3571 . . . . . . . . 9 mCN mCN mVR
1210, 11syl 17 . . . . . . . 8 mCN mVR mCN mVR
1312adantl 467 . . . . . . 7 mCN mVR mCN mVR
1413s1cld 12685 . . . . . 6 mCN mVR Word mCN mVR
15 n0i 3704 . . . . . . . . . 10
16 fvprc 5814 . . . . . . . . . . . . 13 mRSubst
171, 16syl5eq 2469 . . . . . . . . . . . 12
1817rneqd 5019 . . . . . . . . . . 11
19 rn0 5043 . . . . . . . . . . 11
2018, 19syl6eq 2473 . . . . . . . . . 10
2115, 20nsyl2 130 . . . . . . . . 9
2221adantr 466 . . . . . . . 8
2322adantr 466 . . . . . . 7 mCN mVR
24 eqid 2423 . . . . . . . 8 mCN mCN
25 eqid 2423 . . . . . . . 8 mVR mVR
2624, 25, 2mrexval 30086 . . . . . . 7 mREx Word mCN mVR
2723, 26syl 17 . . . . . 6 mCN mVR mREx Word mCN mVR
2814, 27eleqtrrd 2504 . . . . 5 mCN mVR mREx
29 fvco3 5897 . . . . 5 mRExmREx mREx
309, 28, 29syl2anc 665 . . . 4 mCN mVR
311, 2, 25, 24mrsubcn 30104 . . . . . 6 mCN mVR
3231adantll 718 . . . . 5 mCN mVR
3332fveq2d 5824 . . . 4 mCN mVR
341, 2, 25, 24mrsubcn 30104 . . . . 5 mCN mVR
3534adantlr 719 . . . 4 mCN mVR
3630, 33, 353eqtrd 2461 . . 3 mCN mVR
3736ralrimiva 2774 . 2 mCN mVR
381, 2mrsubccat 30103 . . . . . . . 8 mREx mREx ++ ++
39383expb 1206 . . . . . . 7 mREx mREx ++ ++
4039adantll 718 . . . . . 6 mREx mREx ++ ++
4140fveq2d 5824 . . . . 5 mREx mREx ++ ++
42 simpll 758 . . . . . 6 mREx mREx
436adantr 466 . . . . . . 7 mREx mREx mRExmREx
44 simprl 762 . . . . . . 7 mREx mREx mREx
4543, 44ffvelrnd 5977 . . . . . 6 mREx mREx mREx
46 simprr 764 . . . . . . 7 mREx mREx mREx
4743, 46ffvelrnd 5977 . . . . . 6 mREx mREx mREx
481, 2mrsubccat 30103 . . . . . 6 mREx mREx ++ ++
4942, 45, 47, 48syl3anc 1264 . . . . 5 mREx mREx ++ ++
5041, 49eqtrd 2457 . . . 4 mREx mREx ++ ++
5122, 26syl 17 . . . . . . . . 9 mREx Word mCN mVR
5251adantr 466 . . . . . . . 8 mREx mREx mREx Word mCN mVR
5344, 52eleqtrd 2503 . . . . . . 7 mREx mREx Word mCN mVR
5446, 52eleqtrd 2503 . . . . . . 7 mREx mREx Word mCN mVR
55 ccatcl 12663 . . . . . . 7 Word mCN mVR Word mCN mVR ++ Word mCN mVR
5653, 54, 55syl2anc 665 . . . . . 6 mREx mREx ++ Word mCN mVR
5756, 52eleqtrrd 2504 . . . . 5 mREx mREx ++ mREx
58 fvco3 5897 . . . . 5 mRExmREx ++ mREx ++ ++
5943, 57, 58syl2anc 665 . . . 4 mREx mREx ++ ++
60 fvco3 5897 . . . . . 6 mRExmREx mREx
6143, 44, 60syl2anc 665 . . . . 5 mREx mREx
62 fvco3 5897 . . . . . 6 mRExmREx mREx
6343, 46, 62syl2anc 665 . . . . 5 mREx mREx
6461, 63oveq12d 6262 . . . 4 mREx mREx ++ ++
6550, 59, 643eqtr4d 2467 . . 3 mREx mREx ++ ++
6665ralrimivva 2781 . 2 mREx mREx ++ ++
671, 2, 25, 24elmrsubrn 30105 . . 3 mRExmREx mCN mVR mREx mREx ++ ++
6822, 67syl 17 . 2 mRExmREx mCN mVR mREx mREx ++ ++
698, 37, 66, 68mpbir3and 1188 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2709  cvv 3017   cdif 3371   cun 3372  c0 3699   crn 4792   ccom 4795  wf 5535  cfv 5539  (class class class)co 6244  Word cword 12599   ++ cconcat 12601  cs1 12602  mCNcmcn 30045  mVRcmvar 30046  mRExcmrex 30051  mRSubstcmrsub 30055 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-int 4194  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-1st 6746  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-card 8320  df-cda 8544  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-2 10614  df-n0 10816  df-z 10884  df-uz 11106  df-fz 11731  df-fzo 11862  df-seq 12159  df-hash 12461  df-word 12607  df-lsw 12608  df-concat 12609  df-s1 12610  df-substr 12611  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-ress 15066  df-plusg 15141  df-0g 15278  df-gsum 15279  df-mgm 16426  df-sgrp 16465  df-mnd 16475  df-mhm 16520  df-submnd 16521  df-frmd 16571  df-vrmd 16572  df-mrex 30071  df-mrsub 30075 This theorem is referenced by:  msubco  30116
 Copyright terms: Public domain W3C validator