Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  catcfuccl Structured version   Unicode version

Theorem catcfuccl 15942
 Description: The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
catcfuccl.c CatCat
catcfuccl.b
catcfuccl.o FuncCat
catcfuccl.u WUni
catcfuccl.1
catcfuccl.x
catcfuccl.y
Assertion
Ref Expression
catcfuccl

Proof of Theorem catcfuccl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcfuccl.o . . . . 5 FuncCat
2 eqid 2423 . . . . 5
3 eqid 2423 . . . . 5 Nat Nat
4 eqid 2423 . . . . 5
5 eqid 2423 . . . . 5 comp comp
6 inss2 3621 . . . . . 6
7 catcfuccl.x . . . . . . 7
8 catcfuccl.c . . . . . . . 8 CatCat
9 catcfuccl.b . . . . . . . 8
10 catcfuccl.u . . . . . . . 8 WUni
118, 9, 10catcbas 15930 . . . . . . 7
127, 11eleqtrd 2503 . . . . . 6
136, 12sseldi 3400 . . . . 5
14 catcfuccl.y . . . . . . 7
1514, 11eleqtrd 2503 . . . . . 6
166, 15sseldi 3400 . . . . 5
17 eqidd 2424 . . . . 5 Nat Nat comp Nat Nat comp
181, 2, 3, 4, 5, 13, 16, 17fucval 15801 . . . 4 Nat comp Nat Nat comp
19 df-base 15064 . . . . . . 7 Slot
20 catcfuccl.1 . . . . . . . 8
2110, 20wunndx 15075 . . . . . . 7
2219, 10, 21wunstr 15078 . . . . . 6
23 inss1 3620 . . . . . . . 8
2423, 12sseldi 3400 . . . . . . 7
2523, 15sseldi 3400 . . . . . . 7
2610, 24, 25wunfunc 15742 . . . . . 6
2710, 22, 26wunop 9093 . . . . 5
28 df-hom 15152 . . . . . . 7 Slot ;
2928, 10, 21wunstr 15078 . . . . . 6
3010, 24, 25wunnat 15799 . . . . . 6 Nat
3110, 29, 30wunop 9093 . . . . 5 Nat
32 df-cco 15153 . . . . . . 7 comp Slot ;
3332, 10, 21wunstr 15078 . . . . . 6 comp
3410, 26, 26wunxp 9095 . . . . . . . 8
3510, 34, 26wunxp 9095 . . . . . . 7
3632, 10, 25wunstr 15078 . . . . . . . . . . . . . 14 comp
3710, 36wunrn 9100 . . . . . . . . . . . . 13 comp
3810, 37wununi 9077 . . . . . . . . . . . 12 comp
3910, 38wunrn 9100 . . . . . . . . . . 11 comp
4010, 39wununi 9077 . . . . . . . . . 10 comp
4110, 40wunpw 9078 . . . . . . . . 9 comp
4219, 10, 24wunstr 15078 . . . . . . . . 9
4310, 41, 42wunmap 9097 . . . . . . . 8 comp
4410, 30wunrn 9100 . . . . . . . . . 10 Nat
4510, 44wununi 9077 . . . . . . . . 9 Nat
4610, 45, 45wunxp 9095 . . . . . . . 8 Nat Nat
4710, 43, 46wunpm 9096 . . . . . . 7 comp Nat Nat
48 fvex 5830 . . . . . . . . . . 11
49 fvex 5830 . . . . . . . . . . . . . 14
50 ovex 6272 . . . . . . . . . . . . . . . . 17 comp
51 ovex 6272 . . . . . . . . . . . . . . . . . . . 20 Nat
5251rnex 6680 . . . . . . . . . . . . . . . . . . 19 Nat
5352uniex 6540 . . . . . . . . . . . . . . . . . 18 Nat
5453, 53xpex 6548 . . . . . . . . . . . . . . . . 17 Nat Nat
55 eqid 2423 . . . . . . . . . . . . . . . . . . . . 21 comp comp
56 ovssunirn 6273 . . . . . . . . . . . . . . . . . . . . . . . 24 comp comp
57 ovssunirn 6273 . . . . . . . . . . . . . . . . . . . . . . . . 25 comp comp
58 rnss 5020 . . . . . . . . . . . . . . . . . . . . . . . . 25 comp comp comp comp
59 uniss 4178 . . . . . . . . . . . . . . . . . . . . . . . . 25 comp comp comp comp
6057, 58, 59mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 comp comp
6156, 60sstri 3411 . . . . . . . . . . . . . . . . . . . . . . 23 comp comp
62 ovex 6272 . . . . . . . . . . . . . . . . . . . . . . . 24 comp
6362elpw 3925 . . . . . . . . . . . . . . . . . . . . . . 23 comp comp comp comp
6461, 63mpbir 212 . . . . . . . . . . . . . . . . . . . . . 22 comp comp
6564a1i 11 . . . . . . . . . . . . . . . . . . . . 21 comp comp
6655, 65fmpti 5999 . . . . . . . . . . . . . . . . . . . 20 comp comp
67 fvex 5830 . . . . . . . . . . . . . . . . . . . . . . . . . 26 comp
6867rnex 6680 . . . . . . . . . . . . . . . . . . . . . . . . 25 comp
6968uniex 6540 . . . . . . . . . . . . . . . . . . . . . . . 24 comp
7069rnex 6680 . . . . . . . . . . . . . . . . . . . . . . 23 comp
7170uniex 6540 . . . . . . . . . . . . . . . . . . . . . 22 comp
7271pwex 4545 . . . . . . . . . . . . . . . . . . . . 21 comp
73 fvex 5830 . . . . . . . . . . . . . . . . . . . . 21
7472, 73elmap 7450 . . . . . . . . . . . . . . . . . . . 20 comp comp comp comp
7566, 74mpbir 212 . . . . . . . . . . . . . . . . . . 19 comp comp
7675rgen2w 2722 . . . . . . . . . . . . . . . . . 18 Nat Nat comp comp
77 eqid 2423 . . . . . . . . . . . . . . . . . . 19 Nat Nat comp Nat Nat comp
7877fmpt2 6813 . . . . . . . . . . . . . . . . . 18 Nat Nat comp comp Nat Nat comp Nat Nat comp
7976, 78mpbi 211 . . . . . . . . . . . . . . . . 17 Nat Nat comp Nat Nat comp
80 ovssunirn 6273 . . . . . . . . . . . . . . . . . 18 Nat Nat
81 ovssunirn 6273 . . . . . . . . . . . . . . . . . 18 Nat Nat
82 xpss12 4897 . . . . . . . . . . . . . . . . . 18 Nat Nat Nat Nat Nat Nat Nat Nat
8380, 81, 82mp2an 676 . . . . . . . . . . . . . . . . 17 Nat Nat Nat Nat
84 elpm2r 7439 . . . . . . . . . . . . . . . . 17 comp Nat Nat Nat Nat comp Nat Nat comp Nat Nat Nat Nat Nat Nat comp comp Nat Nat
8550, 54, 79, 83, 84mp4an 677 . . . . . . . . . . . . . . . 16 Nat Nat comp comp Nat Nat
8685sbcth 3252 . . . . . . . . . . . . . . 15 Nat Nat comp comp Nat Nat
87 sbcel1g 3744 . . . . . . . . . . . . . . 15 Nat Nat comp comp Nat Nat Nat Nat comp comp Nat Nat
8886, 87mpbid 213 . . . . . . . . . . . . . 14 Nat Nat comp comp Nat Nat
8949, 88ax-mp 5 . . . . . . . . . . . . 13 Nat Nat comp comp Nat Nat
9089sbcth 3252 . . . . . . . . . . . 12 Nat Nat comp comp Nat Nat
91 sbcel1g 3744 . . . . . . . . . . . 12 Nat Nat comp comp Nat Nat Nat Nat comp comp Nat Nat
9290, 91mpbid 213 . . . . . . . . . . 11 Nat Nat comp comp Nat Nat
9348, 92ax-mp 5 . . . . . . . . . 10 Nat Nat comp comp Nat Nat
9493rgen2w 2722 . . . . . . . . 9 Nat Nat comp comp Nat Nat
95 eqid 2423 . . . . . . . . . 10 Nat Nat comp Nat Nat comp
9695fmpt2 6813 . . . . . . . . 9 Nat Nat comp comp Nat Nat Nat Nat comp comp Nat Nat
9794, 96mpbi 211 . . . . . . . 8 Nat Nat comp comp Nat Nat
9897a1i 11 . . . . . . 7 Nat Nat comp comp Nat Nat
9910, 35, 47, 98wunf 9098 . . . . . 6 Nat Nat comp
10010, 33, 99wunop 9093 . . . . 5 comp Nat Nat comp
10110, 27, 31, 100wuntp 9082 . . . 4 Nat comp Nat Nat comp
10218, 101eqeltrd 2501 . . 3
1031, 13, 16fuccat 15813 . . 3
104102, 103elind 3588 . 2
105104, 11eleqtrrd 2504 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wcel 1872  wral 2709  cvv 3017  wsbc 3237  csb 3333   cin 3373   wss 3374  cpw 3919  ctp 3940  cop 3942  cuni 4157   cmpt 4420   cxp 4789   crn 4792  wf 5535  cfv 5539  (class class class)co 6244   cmpt2 6246  com 6645  c1st 6744  c2nd 6745   cmap 7422   cpm 7423  WUnicwun 9071  c1 9486  c4 10607  c5 10608  ;cdc 10997  cnx 15056  cbs 15059   chom 15139  compcco 15140  ccat 15508   cfunc 15697   Nat cnat 15784   FuncCat cfuc 15785  CatCatccatc 15927 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-inf2 8094  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-fal 1443  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-omul 7137  df-er 7313  df-ec 7315  df-qs 7319  df-map 7424  df-pm 7425  df-ixp 7473  df-en 7520  df-dom 7521  df-sdom 7522  df-fin 7523  df-wun 9073  df-ni 9243  df-pli 9244  df-mi 9245  df-lti 9246  df-plpq 9279  df-mpq 9280  df-ltpq 9281  df-enq 9282  df-nq 9283  df-erq 9284  df-plq 9285  df-mq 9286  df-1nq 9287  df-rq 9288  df-ltnq 9289  df-np 9352  df-plp 9354  df-ltp 9356  df-enr 9426  df-nr 9427  df-c 9491  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-3 10615  df-4 10616  df-5 10617  df-6 10618  df-7 10619  df-8 10620  df-9 10621  df-10 10622  df-n0 10816  df-z 10884  df-dec 10998  df-uz 11106  df-fz 11731  df-struct 15061  df-ndx 15062  df-slot 15063  df-base 15064  df-hom 15152  df-cco 15153  df-cat 15512  df-cid 15513  df-func 15701  df-nat 15786  df-fuc 15787  df-catc 15928 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator