Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isfuna Unicode version

Theorem isfuna 25834
 Description: The class of functors between the categories and . (Contributed by FL, 10-Feb-2008.)
Hypotheses
Ref Expression
isfuna.1
isfuna.2
isfuna.3
isfuna.4
isfuna.5
isfuna.6
isfuna.7
isfuna.8
isfuna.9
isfuna.10
isfuna.11
isfuna.12
Assertion
Ref Expression
isfuna
Distinct variable groups:   ,,,   ,   ,   ,   ,,,,,   ,,,,,
Allowed substitution hints:   (,,,)   (,)   (,,,)   (,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)   (,,,,)

Proof of Theorem isfuna
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 5861 . 2
2 fveq2 5525 . . . . . . 7
32dmeqd 4881 . . . . . 6
4 isfuna.8 . . . . . 6
53, 4syl6eqr 2333 . . . . 5
6 fveq2 5525 . . . . . . 7
76dmeqd 4881 . . . . . 6
8 isfuna.2 . . . . . 6
97, 8syl6eqr 2333 . . . . 5
105, 9oveqan12rd 5878 . . . 4
11 fveq2 5525 . . . . . . . 8
1211dmeqd 4881 . . . . . . 7
13 isfuna.1 . . . . . . . . 9
1413a1i 10 . . . . . . . 8
1514eqcomd 2288 . . . . . . 7
1612, 15sylan9eq 2335 . . . . . 6
17 fveq2 5525 . . . . . . . . . 10
1817dmeqd 4881 . . . . . . . . 9
19 isfuna.7 . . . . . . . . 9
2018, 19syl6eqr 2333 . . . . . . . 8
2120adantl 452 . . . . . . 7
2211fveq1d 5527 . . . . . . . . . 10
2322fveq2d 5529 . . . . . . . . 9
2423eqeq1d 2291 . . . . . . . 8
25 isfuna.5 . . . . . . . . . . . . 13
2625a1i 10 . . . . . . . . . . . 12
2726eqcomd 2288 . . . . . . . . . . 11
2827fveq1d 5527 . . . . . . . . . 10
2928fveq2d 5529 . . . . . . . . 9
30 isfuna.11 . . . . . . . . . . 11
3117, 30syl6eqr 2333 . . . . . . . . . 10
3231fveq1d 5527 . . . . . . . . 9
3329, 32eqeq12d 2297 . . . . . . . 8
3424, 33sylan9bb 680 . . . . . . 7
3521, 34rexeqbidv 2749 . . . . . 6
3616, 35raleqbidv 2748 . . . . 5
379adantr 451 . . . . . . 7
3811, 25syl6eqr 2333 . . . . . . . . . 10
39 isfuna.3 . . . . . . . . . . . 12
406, 39syl6eqr 2333 . . . . . . . . . . 11
4140fveq1d 5527 . . . . . . . . . 10
4238, 41fveq12d 5531 . . . . . . . . 9
4342fveq2d 5529 . . . . . . . 8
4417fveq1d 5527 . . . . . . . . 9
452fveq1d 5527 . . . . . . . . . 10
4645fveq2d 5529 . . . . . . . . 9
4730a1i 10 . . . . . . . . . . 11
4847eqcomd 2288 . . . . . . . . . 10
49 isfuna.9 . . . . . . . . . . . . 13
5049a1i 10 . . . . . . . . . . . 12
5150eqcomd 2288 . . . . . . . . . . 11
5251fveq1d 5527 . . . . . . . . . 10
5348, 52fveq12d 5531 . . . . . . . . 9
5444, 46, 533eqtrd 2319 . . . . . . . 8
5543, 54eqeqan12d 2298 . . . . . . 7
5637, 55raleqbidv 2748 . . . . . 6
57 fveq2 5525 . . . . . . . . . . . 12
5857fveq1d 5527 . . . . . . . . . . 11
5911, 58fveq12d 5531 . . . . . . . . . 10
6059fveq2d 5529 . . . . . . . . 9
6160eqeq1d 2291 . . . . . . . 8
627, 61raleqbidv 2748 . . . . . . 7
638a1i 10 . . . . . . . . . . 11
6463eleq2d 2350 . . . . . . . . . 10
6564bicomd 192 . . . . . . . . 9
66 isfuna.4 . . . . . . . . . . . . . . 15
6766a1i 10 . . . . . . . . . . . . . 14
6867eqcomd 2288 . . . . . . . . . . . . 13
6968fveq1d 5527 . . . . . . . . . . . 12
7027, 69fveq12d 5531 . . . . . . . . . . 11
7170fveq2d 5529 . . . . . . . . . 10
72 fveq2 5525 . . . . . . . . . . . . 13
73 isfuna.10 . . . . . . . . . . . . 13
7472, 73syl6eqr 2333 . . . . . . . . . . . 12
7574fveq1d 5527 . . . . . . . . . . 11
7631, 75fveq12d 5531 . . . . . . . . . 10
7771, 76eqeq12d 2297 . . . . . . . . 9
7865, 77imbi12d 311 . . . . . . . 8
7978ralbidv2 2565 . . . . . . 7
8062, 79sylan9bb 680 . . . . . 6
8156, 80anbi12d 691 . . . . 5
8257, 66syl6eqr 2333 . . . . . . . . . . 11
8382fveq1d 5527 . . . . . . . . . 10
8483, 41eqeq12d 2297 . . . . . . . . 9
8584adantr 451 . . . . . . . 8
86 fveq2 5525 . . . . . . . . . . . 12
87 isfuna.6 . . . . . . . . . . . 12
8886, 87syl6eqr 2333 . . . . . . . . . . 11
8988oveqd 5875 . . . . . . . . . 10
9089fveq2d 5529 . . . . . . . . 9
91 fveq2 5525 . . . . . . . . . . 11
92 isfuna.12 . . . . . . . . . . 11
9391, 92syl6eqr 2333 . . . . . . . . . 10
9493oveqd 5875 . . . . . . . . 9
9590, 94eqeqan12d 2298 . . . . . . . 8
9685, 95imbi12d 311 . . . . . . 7
9737, 96raleqbidv 2748 . . . . . 6
9837, 97raleqbidv 2748 . . . . 5
9936, 81, 983anbi123d 1252 . . . 4
10010, 99rabeqbidv 2783 . . 3
101 df-funcOLD 25833 . . 3
102 ovex 5883 . . . 4
103102rabex 4165 . . 3
104100, 101, 103ovmpt2a 5978 . 2
1051, 104syl5eqr 2329 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1623   wcel 1684  wral 2543  wrex 2544  crab 2547  cop 3643   cdm 4689  cfv 5255  (class class class)co 5858   cmap 6772  cdom_ 25712  ccod_ 25713  cid_ 25714  co_ 25715   ccatOLD 25752  cfuncOLD 25831 This theorem is referenced by:  isfunb  25835 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-funcOLD 25833
 Copyright terms: Public domain W3C validator