Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmptcof2 Unicode version

Theorem fmptcof2 23479
 Description: Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) (Revised by Thierry Arnoux, 10-May-2017.)
Hypotheses
Ref Expression
fmptcof2.1
fmptcof2.2
fmptcof2.3
fmptcof2.4
fmptcof2.5
fmptcof2.6
fmptcof2.7
Assertion
Ref Expression
fmptcof2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   ()   ()   ()   ()   (,)   (,)

Proof of Theorem fmptcof2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 5274 . 2
2 funmpt 5393 . . 3
3 funrel 5375 . . 3
42, 3ax-mp 8 . 2
5 nfv 1624 . . . . 5
6 fmptcof2.3 . . . . . . . . . . . . 13
7 fmptcof2.1 . . . . . . . . . . . . 13
8 fmptcof2.2 . . . . . . . . . . . . 13
9 fmptcof2.4 . . . . . . . . . . . . . 14
109r19.21bi 2726 . . . . . . . . . . . . 13
11 eqid 2366 . . . . . . . . . . . . 13
126, 7, 8, 10, 11fmptdF 23471 . . . . . . . . . . . 12
13 fmptcof2.5 . . . . . . . . . . . . 13
1413feq1d 5484 . . . . . . . . . . . 12
1512, 14mpbird 223 . . . . . . . . . . 11
16 ffun 5497 . . . . . . . . . . 11
1715, 16syl 15 . . . . . . . . . 10
18 funbrfv 5668 . . . . . . . . . . 11
1918imp 418 . . . . . . . . . 10
2017, 19sylan 457 . . . . . . . . 9
2120eqcomd 2371 . . . . . . . 8
2221a1d 22 . . . . . . 7
2322expimpd 586 . . . . . 6
2423pm4.71rd 616 . . . . 5
255, 24exbid 1779 . . . 4
26 fvex 5646 . . . . . 6
27 breq2 4129 . . . . . . 7
28 breq1 4128 . . . . . . 7
2927, 28anbi12d 691 . . . . . 6
3026, 29ceqsexv 2908 . . . . 5
31 funfvbrb 5745 . . . . . . . . 9
3217, 31syl 15 . . . . . . . 8
33 fdm 5499 . . . . . . . . . 10
3415, 33syl 15 . . . . . . . . 9
3534eleq2d 2433 . . . . . . . 8
3632, 35bitr3d 246 . . . . . . 7
3713fveq1d 5634 . . . . . . . 8
38 fmptcof2.6 . . . . . . . 8
39 eqidd 2367 . . . . . . . 8
4037, 38, 39breq123d 4139 . . . . . . 7
4136, 40anbi12d 691 . . . . . 6
42 nfcv 2502 . . . . . . . . . 10
4342, 7nfel 2510 . . . . . . . . . . 11
44 nfmpt1 4211 . . . . . . . . . . . . . . 15
4544, 42nffv 5639 . . . . . . . . . . . . . 14
46 nfcv 2502 . . . . . . . . . . . . . . 15
478, 46nfmpt 4210 . . . . . . . . . . . . . 14
48 nfcv 2502 . . . . . . . . . . . . . 14
4945, 47, 48nfbr 4169 . . . . . . . . . . . . 13
50 nfcsb1v 3199 . . . . . . . . . . . . . 14
5150nfeq2 2513 . . . . . . . . . . . . 13
5249, 51nfbi 1844 . . . . . . . . . . . 12
536, 52nfim 1820 . . . . . . . . . . 11
5443, 53nfim 1820 . . . . . . . . . 10
55 eleq1 2426 . . . . . . . . . . 11
56 fveq2 5632 . . . . . . . . . . . . . 14
5756breq1d 4135 . . . . . . . . . . . . 13
58 csbeq1a 3175 . . . . . . . . . . . . . 14
5958eqeq2d 2377 . . . . . . . . . . . . 13
6057, 59bibi12d 312 . . . . . . . . . . . 12
6160imbi2d 307 . . . . . . . . . . 11
6255, 61imbi12d 311 . . . . . . . . . 10
63 vex 2876 . . . . . . . . . . . . 13
64 simpl 443 . . . . . . . . . . . . . . . 16
6564eleq1d 2432 . . . . . . . . . . . . . . 15
66 simpr 447 . . . . . . . . . . . . . . . 16
67 fmptcof2.7 . . . . . . . . . . . . . . . . 17
6867adantr 451 . . . . . . . . . . . . . . . 16
6966, 68eqeq12d 2380 . . . . . . . . . . . . . . 15
7065, 69anbi12d 691 . . . . . . . . . . . . . 14
71 df-mpt 4181 . . . . . . . . . . . . . 14
7270, 71brabga 4382 . . . . . . . . . . . . 13
7310, 63, 72sylancl 643 . . . . . . . . . . . 12
74 simpr 447 . . . . . . . . . . . . . 14
757fvmpt2f 23474 . . . . . . . . . . . . . 14
7674, 10, 75syl2anc 642 . . . . . . . . . . . . 13
7776breq1d 4135 . . . . . . . . . . . 12
7810biantrurd 494 . . . . . . . . . . . 12
7973, 77, 783bitr4d 276 . . . . . . . . . . 11
8079expcom 424 . . . . . . . . . 10
8142, 54, 62, 80vtoclgf 2927 . . . . . . . . 9
8281pm2.43i 43 . . . . . . . 8
8382impcom 419 . . . . . . 7
8483pm5.32da 622 . . . . . 6
8541, 84bitrd 244 . . . . 5
8630, 85syl5bb 248 . . . 4
8725, 86bitrd 244 . . 3
88 vex 2876 . . . 4
8988, 63opelco 4956 . . 3
90 df-mpt 4181 . . . . 5
9190eleq2i 2430 . . . 4
9250nfeq2 2513 . . . . . 6
9343, 92nfan 1834 . . . . 5
94 nfv 1624 . . . . 5
9558eqeq2d 2377 . . . . . 6
9655, 95anbi12d 691 . . . . 5
97 eqeq1 2372 . . . . . 6
9897anbi2d 684 . . . . 5
9993, 94, 88, 63, 96, 98opelopabf 4392 . . . 4
10091, 99bitri 240 . . 3
10187, 89, 1003bitr4g 279 . 2
1021, 4, 101eqrelrdv 4886 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wex 1546  wnf 1549   wceq 1647   wcel 1715  wnfc 2489  wral 2628  cvv 2873  csb 3167  cop 3732   class class class wbr 4125  copab 4178   cmpt 4179   cdm 4792   ccom 4796   wrel 4797   wfun 5352  wf 5354  cfv 5358 This theorem is referenced by:  fcomptf  23480  esumf1o  23910 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-fv 5366
 Copyright terms: Public domain W3C validator