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

Theorem msubff1 30266
 Description: When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
msubff1.v mVR
msubff1.r mREx
msubff1.s mSubst
msubff1.e mEx
Assertion
Ref Expression
msubff1 mFS

Proof of Theorem msubff1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 msubff1.v . . . 4 mVR
2 msubff1.r . . . 4 mREx
3 msubff1.s . . . 4 mSubst
4 msubff1.e . . . 4 mEx
51, 2, 3, 4msubff 30240 . . 3 mFS
6 mapsspm 7523 . . . 4
76a1i 11 . . 3 mFS
85, 7fssresd 5762 . 2 mFS
9 eqid 2471 . . . . . . . . . . . . 13 mRSubst mRSubst
101, 2, 9mrsubff 30222 . . . . . . . . . . . 12 mFS mRSubst
1110ad2antrr 740 . . . . . . . . . . 11 mFS mRSubst
12 simplrl 778 . . . . . . . . . . . 12 mFS
136, 12sseldi 3416 . . . . . . . . . . 11 mFS
1411, 13ffvelrnd 6038 . . . . . . . . . 10 mFS mRSubst
15 elmapi 7511 . . . . . . . . . 10 mRSubst mRSubst
16 ffn 5739 . . . . . . . . . 10 mRSubst mRSubst
1714, 15, 163syl 18 . . . . . . . . 9 mFS mRSubst
18 simplrr 779 . . . . . . . . . . . 12 mFS
196, 18sseldi 3416 . . . . . . . . . . 11 mFS
2011, 19ffvelrnd 6038 . . . . . . . . . 10 mFS mRSubst
21 elmapi 7511 . . . . . . . . . 10 mRSubst mRSubst
22 ffn 5739 . . . . . . . . . 10 mRSubst mRSubst
2320, 21, 223syl 18 . . . . . . . . 9 mFS mRSubst
24 simplrr 779 . . . . . . . . . . . . 13 mFS
2524fveq1d 5881 . . . . . . . . . . . 12 mFS mType mType
2612adantr 472 . . . . . . . . . . . . . 14 mFS
27 elmapi 7511 . . . . . . . . . . . . . 14
2826, 27syl 17 . . . . . . . . . . . . 13 mFS
29 ssid 3437 . . . . . . . . . . . . . 14
3029a1i 11 . . . . . . . . . . . . 13 mFS
31 eqid 2471 . . . . . . . . . . . . . . . . . 18 mTC mTC
32 eqid 2471 . . . . . . . . . . . . . . . . . 18 mType mType
331, 31, 32mtyf2 30261 . . . . . . . . . . . . . . . . 17 mFS mTypemTC
3433ad3antrrr 744 . . . . . . . . . . . . . . . 16 mFS mTypemTC
35 simplrl 778 . . . . . . . . . . . . . . . 16 mFS
3634, 35ffvelrnd 6038 . . . . . . . . . . . . . . 15 mFS mType mTC
37 opelxpi 4871 . . . . . . . . . . . . . . 15 mType mTC mType mTC
3836, 37sylancom 680 . . . . . . . . . . . . . 14 mFS mType mTC
3931, 4, 2mexval 30212 . . . . . . . . . . . . . 14 mTC
4038, 39syl6eleqr 2560 . . . . . . . . . . . . 13 mFS mType
411, 2, 3, 4, 9msubval 30235 . . . . . . . . . . . . 13 mType mType mType mRSubstmType
4228, 30, 40, 41syl3anc 1292 . . . . . . . . . . . 12 mFS mType mType mRSubstmType
4318adantr 472 . . . . . . . . . . . . . 14 mFS
44 elmapi 7511 . . . . . . . . . . . . . 14
4543, 44syl 17 . . . . . . . . . . . . 13 mFS
461, 2, 3, 4, 9msubval 30235 . . . . . . . . . . . . 13 mType mType mType mRSubstmType
4745, 30, 40, 46syl3anc 1292 . . . . . . . . . . . 12 mFS mType mType mRSubstmType
4825, 42, 473eqtr3d 2513 . . . . . . . . . . 11 mFS mType mRSubstmType mType mRSubstmType
49 fvex 5889 . . . . . . . . . . . . 13 mType
50 fvex 5889 . . . . . . . . . . . . 13 mRSubstmType
5149, 50opth 4676 . . . . . . . . . . . 12 mType mRSubstmType mType mRSubstmType mType mType mRSubstmType mRSubstmType
5251simprbi 471 . . . . . . . . . . 11 mType mRSubstmType mType mRSubstmType mRSubstmType mRSubstmType
5348, 52syl 17 . . . . . . . . . 10 mFS mRSubstmType mRSubstmType
54 fvex 5889 . . . . . . . . . . . 12 mType
55 vex 3034 . . . . . . . . . . . 12
5654, 55op2nd 6821 . . . . . . . . . . 11 mType
5756fveq2i 5882 . . . . . . . . . 10 mRSubstmType mRSubst
5856fveq2i 5882 . . . . . . . . . 10 mRSubstmType mRSubst
5953, 57, 583eqtr3g 2528 . . . . . . . . 9 mFS mRSubst mRSubst
6017, 23, 59eqfnfvd 5994 . . . . . . . 8 mFS mRSubst mRSubst
611, 2, 9mrsubff1 30224 . . . . . . . . . . 11 mFS mRSubst
62 f1fveq 6181 . . . . . . . . . . 11 mRSubst mRSubst mRSubst
6361, 62sylan 479 . . . . . . . . . 10 mFS mRSubst mRSubst
64 fvres 5893 . . . . . . . . . . . 12 mRSubst mRSubst
65 fvres 5893 . . . . . . . . . . . 12 mRSubst mRSubst
6664, 65eqeqan12d 2487 . . . . . . . . . . 11 mRSubst mRSubst mRSubst mRSubst
6766adantl 473 . . . . . . . . . 10 mFS mRSubst mRSubst mRSubst mRSubst
6863, 67bitr3d 263 . . . . . . . . 9 mFS mRSubst mRSubst
6968adantr 472 . . . . . . . 8 mFS mRSubst mRSubst
7060, 69mpbird 240 . . . . . . 7 mFS
7170fveq1d 5881 . . . . . 6 mFS
7271expr 626 . . . . 5 mFS
7372ralrimdva 2812 . . . 4 mFS
74 fvres 5893 . . . . . 6
75 fvres 5893 . . . . . 6
7674, 75eqeqan12d 2487 . . . . 5
7776adantl 473 . . . 4 mFS
78 ffn 5739 . . . . . . 7
79 ffn 5739 . . . . . . 7
80 eqfnfv 5991 . . . . . . 7
8178, 79, 80syl2an 485 . . . . . 6
8227, 44, 81syl2an 485 . . . . 5
8382adantl 473 . . . 4 mFS
8473, 77, 833imtr4d 276 . . 3 mFS
8584ralrimivva 2814 . 2 mFS
86 dff13 6177 . 2
878, 85, 86sylanbrc 677 1 mFS
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   wceq 1452   wcel 1904  wral 2756   wss 3390  cop 3965   cxp 4837   cres 4841   wfn 5584  wf 5585  wf1 5586  cfv 5589  (class class class)co 6308  c1st 6810  c2nd 6811   cmap 7490   cpm 7491  mVRcmvar 30171  mTypecmty 30172  mTCcmtc 30174  mRExcmrex 30176  mExcmex 30177  mRSubstcmrsub 30180  mSubstcmsub 30181  mFScmfs 30186 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-fzo 11943  df-seq 12252  df-hash 12554  df-word 12711  df-concat 12713  df-s1 12714  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-0g 15418  df-gsum 15419  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-frmd 16711  df-mrex 30196  df-mex 30197  df-mrsub 30200  df-msub 30201  df-mfs 30206 This theorem is referenced by:  msubff1o  30267
 Copyright terms: Public domain W3C validator