Theorem catcoppccl 16052

Description: The category of categories for a weak universe is closed under taking opposites. (Contributed by Mario Carneiro, 12-Jan-2017.)

Hypotheses

Ref	Expression
catcoppccl.c	|- C = (CatCat ` U )
catcoppccl.b	|- B = ( Base ` C )
catcoppccl.o	|- O = (oppCat ` X )
catcoppccl.1	|- ( ph -> U e. WUni )
catcoppccl.2	|- ( ph -> om e. U )
catcoppccl.3	|- ( ph -> X e. B )

Assertion

Ref	Expression
catcoppccl	|- ( ph -> O e. B )

Proof of Theorem catcoppccl

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		catcoppccl.3	. . . . 5 |- ( ph -> X e. B )
2		eqid 2462	. . . . . 6 |- ( Base ` X ) = ( Base ` X )
3		eqid 2462	. . . . . 6 |- ( Hom ` X ) = ( Hom ` X )
4		eqid 2462	. . . . . 6 |- (comp ` X ) = (comp ` X )
5		catcoppccl.o	. . . . . 6 |- O = (oppCat ` X )
6	2, 3, 4, 5	oppcval 15667	. . . . 5 |- ( X e. B -> O = ( ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) sSet <. (comp ` ndx ) , ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) >. ) )
7	1, 6	syl 17	. . . 4 |- ( ph -> O = ( ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) sSet <. (comp ` ndx ) , ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) >. ) )
8		catcoppccl.1	. . . . 5 |- ( ph -> U e. WUni )
9		inss1 3664	. . . . . . 7 |- ( U i^i Cat ) C_ U
10		catcoppccl.c	. . . . . . . . 9 |- C = (CatCat ` U )
11		catcoppccl.b	. . . . . . . . 9 |- B = ( Base ` C )
12	10, 11, 8	catcbas 16041	. . . . . . . 8 |- ( ph -> B = ( U i^i Cat ) )
13	1, 12	eleqtrd 2542	. . . . . . 7 |- ( ph -> X e. ( U i^i Cat ) )
14	9, 13	sseldi 3442	. . . . . 6 |- ( ph -> X e. U )
15		df-hom 15263	. . . . . . . 8 |- Hom = Slot ; 1 4
16		catcoppccl.2	. . . . . . . . 9 |- ( ph -> om e. U )
17	8, 16	wunndx 15186	. . . . . . . 8 |- ( ph -> ndx e. U )
18	15, 8, 17	wunstr 15189	. . . . . . 7 |- ( ph -> ( Hom ` ndx ) e. U )
19	15, 8, 14	wunstr 15189	. . . . . . . 8 |- ( ph -> ( Hom ` X ) e. U )
20	8, 19	wuntpos 9185	. . . . . . 7 |- ( ph -> tpos ( Hom ` X ) e. U )
21	8, 18, 20	wunop 9173	. . . . . 6 |- ( ph -> <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. e. U )
22	8, 14, 21	wunsets 15199	. . . . 5 |- ( ph -> ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) e. U )
23		df-cco 15264	. . . . . . 7 |- comp = Slot ; 1 5
24	23, 8, 17	wunstr 15189	. . . . . 6 |- ( ph -> (comp ` ndx ) e. U )
25		df-base 15175	. . . . . . . . . 10 |- Base = Slot 1
26	25, 8, 14	wunstr 15189	. . . . . . . . 9 |- ( ph -> ( Base ` X ) e. U )
27	8, 26, 26	wunxp 9175	. . . . . . . 8 |- ( ph -> ( ( Base ` X ) X. ( Base ` X ) ) e. U )
28	8, 27, 26	wunxp 9175	. . . . . . 7 |- ( ph -> ( ( ( Base ` X ) X. ( Base ` X ) ) X. ( Base ` X ) ) e. U )
29	23, 8, 14	wunstr 15189	. . . . . . . . . . . . . 14 |- ( ph -> (comp ` X ) e. U )
30	8, 29	wunrn 9180	. . . . . . . . . . . . 13 |- ( ph -> ran (comp ` X ) e. U )
31	8, 30	wununi 9157	. . . . . . . . . . . 12 |- ( ph -> U. ran (comp ` X ) e. U )
32	8, 31	wundm 9179	. . . . . . . . . . 11 |- ( ph -> dom U. ran (comp ` X ) e. U )
33	8, 32	wuncnv 9181	. . . . . . . . . 10 |- ( ph -> `' dom U. ran (comp ` X ) e. U )
34	8	wun0 9169	. . . . . . . . . . 11 |- ( ph -> (/) e. U )
35	8, 34	wunsn 9167	. . . . . . . . . 10 |- ( ph -> { (/) } e. U )
36	8, 33, 35	wunun 9161	. . . . . . . . 9 |- ( ph -> ( `' dom U. ran (comp ` X ) u. { (/) } ) e. U )
37	8, 31	wunrn 9180	. . . . . . . . 9 |- ( ph -> ran U. ran (comp ` X ) e. U )
38	8, 36, 37	wunxp 9175	. . . . . . . 8 |- ( ph -> ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) e. U )
39	8, 38	wunpw 9158	. . . . . . 7 |- ( ph -> ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) e. U )
40		tposssxp 7003	. . . . . . . . . . . 12 |- tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) u. { (/) } ) X. ran ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) )
41		ovssunirn 6344	. . . . . . . . . . . . . . 15 |- ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ U. ran (comp ` X )
42		dmss 5053	. . . . . . . . . . . . . . 15 |- ( ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ U. ran (comp ` X ) -> dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ dom U. ran (comp ` X ) )
43	41, 42	ax-mp 5	. . . . . . . . . . . . . 14 |- dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ dom U. ran (comp ` X )
44		cnvss 5026	. . . . . . . . . . . . . 14 |- ( dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ dom U. ran (comp ` X ) -> `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ `' dom U. ran (comp ` X ) )
45		unss1 3615	. . . . . . . . . . . . . 14 |- ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ `' dom U. ran (comp ` X ) -> ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) u. { (/) } ) C_ ( `' dom U. ran (comp ` X ) u. { (/) } ) )
46	43, 44, 45	mp2b 10	. . . . . . . . . . . . 13 |- ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) u. { (/) } ) C_ ( `' dom U. ran (comp ` X ) u. { (/) } )
47		rnss 5082	. . . . . . . . . . . . . 14 |- ( ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ U. ran (comp ` X ) -> ran ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ran U. ran (comp ` X ) )
48	41, 47	ax-mp 5	. . . . . . . . . . . . 13 |- ran ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ran U. ran (comp ` X )
49		xpss12 4959	. . . . . . . . . . . . 13 |- ( ( ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) u. { (/) } ) C_ ( `' dom U. ran (comp ` X ) u. { (/) } ) /\ ran ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ran U. ran (comp ` X ) ) -> ( ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) u. { (/) } ) X. ran ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) C_ ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) )
50	46, 48, 49	mp2an 683	. . . . . . . . . . . 12 |- ( ( `' dom ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) u. { (/) } ) X. ran ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) C_ ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) )
51	40, 50	sstri 3453	. . . . . . . . . . 11 |- tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) )
52		elpw2g 4580	. . . . . . . . . . . 12 |- ( ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) e. U -> (tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) <-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) ) )
53	38, 52	syl 17	. . . . . . . . . . 11 |- ( ph -> (tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) <-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) ) )
54	51, 53	mpbiri 241	. . . . . . . . . 10 |- ( ph -> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) )
55	54	ralrimivw 2815	. . . . . . . . 9 |- ( ph -> A. y e. ( Base ` X )tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) )
56	55	ralrimivw 2815	. . . . . . . 8 |- ( ph -> A. x e. ( ( Base ` X ) X. ( Base ` X ) ) A. y e. ( Base ` X )tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) )
57		eqid 2462	. . . . . . . . 9 |- ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) = ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) )
58	57	fmpt2 6887	. . . . . . . 8 |- ( A. x e. ( ( Base ` X ) X. ( Base ` X ) ) A. y e. ( Base ` X )tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) <-> ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) : ( ( ( Base ` X ) X. ( Base ` X ) ) X. ( Base ` X ) ) --> ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) )
59	56, 58	sylib 201	. . . . . . 7 |- ( ph -> ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) : ( ( ( Base ` X ) X. ( Base ` X ) ) X. ( Base ` X ) ) --> ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) )
60	8, 28, 39, 59	wunf 9178	. . . . . 6 |- ( ph -> ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) e. U )
61	8, 24, 60	wunop 9173	. . . . 5 |- ( ph -> <. (comp ` ndx ) , ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) >. e. U )
62	8, 22, 61	wunsets 15199	. . . 4 |- ( ph -> ( ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) sSet <. (comp ` ndx ) , ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) ) >. ) e. U )
63	7, 62	eqeltrd 2540	. . 3 |- ( ph -> O e. U )
64		inss2 3665	. . . . 5 |- ( U i^i Cat ) C_ Cat
65	64, 13	sseldi 3442	. . . 4 |- ( ph -> X e. Cat )
66	5	oppccat 15676	. . . 4 |- ( X e. Cat -> O e. Cat )
67	65, 66	syl 17	. . 3 |- ( ph -> O e. Cat )
68	63, 67	elind 3630	. 2 |- ( ph -> O e. ( U i^i Cat ) )
69	68, 12	eleqtrrd 2543	1 |- ( ph -> O e. B )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   e. wcel 1898   A.wral 2749   u. cun 3414   i^i cin 3415   C_ wss 3416   (/)c0 3743   ~Pcpw 3963   {csn 3980   <.cop 3986   U.cuni 4212   X. cxp 4851   `'ccnv 4852   dom cdm 4853   ran crn 4854   -->wf 5597   ` cfv 5601  (class class class)co 6315   |-> cmpt2 6317   omcom 6719   1stc1st 6818   2ndc2nd 6819  tpos ctpos 6998  WUnicwun 9151   1c1 9566   4c4 10689   5c5 10690  ;cdc 11080   ndxcnx 15167   sSet csts 15168   Basecbs 15170   Hom chom 15250  compcco 15251   Catccat 15619  oppCatcoppc 15665  CatCatccatc 16038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-tpos 6999  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-omul 7213  df-er 7389  df-ec 7391  df-qs 7395  df-map 7500  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-wun 9153  df-ni 9323  df-pli 9324  df-mi 9325  df-lti 9326  df-plpq 9359  df-mpq 9360  df-ltpq 9361  df-enq 9362  df-nq 9363  df-erq 9364  df-plq 9365  df-mq 9366  df-1nq 9367  df-rq 9368  df-ltnq 9369  df-np 9432  df-plp 9434  df-ltp 9436  df-enr 9506  df-nr 9507  df-c 9571  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-fz 11814  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-hom 15263  df-cco 15264  df-cat 15623  df-cid 15624  df-oppc 15666  df-catc 16039

This theorem is referenced by: (None)