Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fmptco Unicode version

Theorem fmptco 5595
 Description: Composition of two functions expressed as ordered-pair class abstractions. If has the equation ( x + 2 ) and the equation ( 3 * z ) then has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
fmptco.1
fmptco.2
fmptco.3
fmptco.4
Assertion
Ref Expression
fmptco
Distinct variable groups:   ,   ,,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   (,)   (,)

Proof of Theorem fmptco
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5046 . 2
2 funmpt 5170 . . 3
3 funrel 5149 . . 3
42, 3ax-mp 5 . 2
5 fmptco.1 . . . . . . . . . . . . 13
6 eqid 2140 . . . . . . . . . . . . 13
75, 6fmptd 5583 . . . . . . . . . . . 12
8 fmptco.2 . . . . . . . . . . . . 13
98feq1d 5268 . . . . . . . . . . . 12
107, 9mpbird 166 . . . . . . . . . . 11
11 ffun 5284 . . . . . . . . . . 11
1210, 11syl 14 . . . . . . . . . 10
13 funbrfv 5469 . . . . . . . . . . 11
1413imp 123 . . . . . . . . . 10
1512, 14sylan 281 . . . . . . . . 9
1615eqcomd 2146 . . . . . . . 8
1716a1d 22 . . . . . . 7
1817expimpd 361 . . . . . 6
1918pm4.71rd 392 . . . . 5
2019exbidv 1798 . . . 4
21 exsimpl 1597 . . . . . . 7
22 isset 2696 . . . . . . 7
2321, 22sylibr 133 . . . . . 6
2423a1i 9 . . . . 5
2512adantr 274 . . . . . . . 8
26 fdm 5287 . . . . . . . . . . 11
2710, 26syl 14 . . . . . . . . . 10
2827eleq2d 2210 . . . . . . . . 9
2928biimpar 295 . . . . . . . 8
30 funfvex 5447 . . . . . . . 8
3125, 29, 30syl2anc 409 . . . . . . 7
3231adantrr 471 . . . . . 6
3332ex 114 . . . . 5
34 breq2 3942 . . . . . . . . 9
35 breq1 3941 . . . . . . . . 9
3634, 35anbi12d 465 . . . . . . . 8
3736ceqsexgv 2819 . . . . . . 7
38 funfvbrb 5542 . . . . . . . . . . 11
3912, 38syl 14 . . . . . . . . . 10
4039, 28bitr3d 189 . . . . . . . . 9
418fveq1d 5432 . . . . . . . . . 10
42 fmptco.3 . . . . . . . . . 10
43 eqidd 2141 . . . . . . . . . 10
4441, 42, 43breq123d 3952 . . . . . . . . 9
4540, 44anbi12d 465 . . . . . . . 8
46 nfcv 2282 . . . . . . . . . . 11
47 nfv 1509 . . . . . . . . . . . 12
48 nffvmpt1 5441 . . . . . . . . . . . . . 14
49 nfcv 2282 . . . . . . . . . . . . . 14
50 nfcv 2282 . . . . . . . . . . . . . 14
5148, 49, 50nfbr 3983 . . . . . . . . . . . . 13
52 nfcsb1v 3041 . . . . . . . . . . . . . 14
5352nfeq2 2294 . . . . . . . . . . . . 13
5451, 53nfbi 1569 . . . . . . . . . . . 12
5547, 54nfim 1552 . . . . . . . . . . 11
56 fveq2 5430 . . . . . . . . . . . . . 14
5756breq1d 3948 . . . . . . . . . . . . 13
58 csbeq1a 3017 . . . . . . . . . . . . . 14
5958eqeq2d 2152 . . . . . . . . . . . . 13
6057, 59bibi12d 234 . . . . . . . . . . . 12
6160imbi2d 229 . . . . . . . . . . 11
62 vex 2693 . . . . . . . . . . . . . 14
63 simpl 108 . . . . . . . . . . . . . . . . 17
6463eleq1d 2209 . . . . . . . . . . . . . . . 16
65 simpr 109 . . . . . . . . . . . . . . . . 17
66 fmptco.4 . . . . . . . . . . . . . . . . . 18
6766adantr 274 . . . . . . . . . . . . . . . . 17
6865, 67eqeq12d 2155 . . . . . . . . . . . . . . . 16
6964, 68anbi12d 465 . . . . . . . . . . . . . . 15
70 df-mpt 4000 . . . . . . . . . . . . . . 15
7169, 70brabga 4195 . . . . . . . . . . . . . 14
725, 62, 71sylancl 410 . . . . . . . . . . . . 13
73 simpr 109 . . . . . . . . . . . . . . 15
746fvmpt2 5513 . . . . . . . . . . . . . . 15
7573, 5, 74syl2anc 409 . . . . . . . . . . . . . 14
7675breq1d 3948 . . . . . . . . . . . . 13
775biantrurd 303 . . . . . . . . . . . . 13
7872, 76, 773bitr4d 219 . . . . . . . . . . . 12
7978expcom 115 . . . . . . . . . . 11
8046, 55, 61, 79vtoclgaf 2755 . . . . . . . . . 10
8180impcom 124 . . . . . . . . 9
8281pm5.32da 448 . . . . . . . 8
8345, 82bitrd 187 . . . . . . 7
8437, 83sylan9bbr 459 . . . . . 6
8584ex 114 . . . . 5
8624, 33, 85pm5.21ndd 695 . . . 4
8720, 86bitrd 187 . . 3
88 vex 2693 . . . 4
8988, 62opelco 4720 . . 3
90 df-mpt 4000 . . . . 5
9190eleq2i 2207 . . . 4
92 nfv 1509 . . . . . 6
9352nfeq2 2294 . . . . . 6
9492, 93nfan 1545 . . . . 5
95 nfv 1509 . . . . 5
96 eleq1 2203 . . . . . 6
9758eqeq2d 2152 . . . . . 6
9896, 97anbi12d 465 . . . . 5
99 eqeq1 2147 . . . . . 6
10099anbi2d 460 . . . . 5
10194, 95, 88, 62, 98, 100opelopabf 4205 . . . 4
10291, 101bitri 183 . . 3
10387, 89, 1023bitr4g 222 . 2
1041, 4, 103eqrelrdv 4644 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wceq 1332  wex 1469   wcel 1481  cvv 2690  csb 3008  cop 3536   class class class wbr 3938  copab 3997   cmpt 3998   cdm 4548   ccom 4552   wrel 4553   wfun 5126  wf 5128  cfv 5132 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-mpt 4000  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-fv 5140 This theorem is referenced by:  fmptcof  5596  cofmpt  5598  fcompt  5599  fcoconst  5600  ofco  6009  lmcn2  12508  cdivcncfap  12815  negfcncf  12817  dvcj  12901  dvfre  12902  dvmptcjx  12914
 Copyright terms: Public domain W3C validator