Theorem catcoppccl 15309

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 2467	. . . . . 6 |- ( Base ` X ) = ( Base ` X )
3		eqid 2467	. . . . . 6 |- ( Hom ` X ) = ( Hom ` X )
4		eqid 2467	. . . . . 6 |- (comp ` X ) = (comp ` X )
5		catcoppccl.o	. . . . . 6 |- O = (oppCat ` X )
6	2, 3, 4, 5	oppcval 14985	. . . . 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 16	. . . 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 3723	. . . . . . 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 15298	. . . . . . . 8 |- ( ph -> B = ( U i^i Cat ) )
13	1, 12	eleqtrd 2557	. . . . . . 7 |- ( ph -> X e. ( U i^i Cat ) )
14	9, 13	sseldi 3507	. . . . . 6 |- ( ph -> X e. U )
15		df-hom 14595	. . . . . . . 8 |- Hom = Slot ; 1 4
16		catcoppccl.2	. . . . . . . . 9 |- ( ph -> om e. U )
17	8, 16	wunndx 14522	. . . . . . . 8 |- ( ph -> ndx e. U )
18	15, 8, 17	wunstr 14525	. . . . . . 7 |- ( ph -> ( Hom ` ndx ) e. U )
19	15, 8, 14	wunstr 14525	. . . . . . . 8 |- ( ph -> ( Hom ` X ) e. U )
20	8, 19	wuntpos 9124	. . . . . . 7 |- ( ph -> tpos ( Hom ` X ) e. U )
21	8, 18, 20	wunop 9112	. . . . . 6 |- ( ph -> <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. e. U )
22	8, 14, 21	wunsets 14533	. . . . 5 |- ( ph -> ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) e. U )
23		df-cco 14596	. . . . . . 7 |- comp = Slot ; 1 5
24	23, 8, 17	wunstr 14525	. . . . . 6 |- ( ph -> (comp ` ndx ) e. U )
25		df-base 14511	. . . . . . . . . 10 |- Base = Slot 1
26	25, 8, 14	wunstr 14525	. . . . . . . . 9 |- ( ph -> ( Base ` X ) e. U )
27	8, 26, 26	wunxp 9114	. . . . . . . 8 |- ( ph -> ( ( Base ` X ) X. ( Base ` X ) ) e. U )
28	8, 27, 26	wunxp 9114	. . . . . . 7 |- ( ph -> ( ( ( Base ` X ) X. ( Base ` X ) ) X. ( Base ` X ) ) e. U )
29	23, 8, 14	wunstr 14525	. . . . . . . . . . . . . 14 |- ( ph -> (comp ` X ) e. U )
30	8, 29	wunrn 9119	. . . . . . . . . . . . 13 |- ( ph -> ran (comp ` X ) e. U )
31	8, 30	wununi 9096	. . . . . . . . . . . 12 |- ( ph -> U. ran (comp ` X ) e. U )
32	8, 31	wundm 9118	. . . . . . . . . . 11 |- ( ph -> dom U. ran (comp ` X ) e. U )
33	8, 32	wuncnv 9120	. . . . . . . . . 10 |- ( ph -> `' dom U. ran (comp ` X ) e. U )
34	8	wun0 9108	. . . . . . . . . . 11 |- ( ph -> (/) e. U )
35	8, 34	wunsn 9106	. . . . . . . . . 10 |- ( ph -> { (/) } e. U )
36	8, 33, 35	wunun 9100	. . . . . . . . 9 |- ( ph -> ( `' dom U. ran (comp ` X ) u. { (/) } ) e. U )
37	8, 31	wunrn 9119	. . . . . . . . 9 |- ( ph -> ran U. ran (comp ` X ) e. U )
38	8, 36, 37	wunxp 9114	. . . . . . . 8 |- ( ph -> ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) e. U )
39	8, 38	wunpw 9097	. . . . . . 7 |- ( ph -> ~P ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) ) e. U )
40		tposssxp 6971	. . . . . . . . . . . 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 6321	. . . . . . . . . . . . . . 15 |- ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ U. ran (comp ` X )
42		dmss 5208	. . . . . . . . . . . . . . 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 5181	. . . . . . . . . . . . . 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 3678	. . . . . . . . . . . . . 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 5237	. . . . . . . . . . . . . 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 5114	. . . . . . . . . . . . 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 672	. . . . . . . . . . . 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 3518	. . . . . . . . . . 11 |- tpos ( <. y , ( 2nd ` x ) >. (comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom U. ran (comp ` X ) u. { (/) } ) X. ran U. ran (comp ` X ) )
52		elpw2g 4616	. . . . . . . . . . . 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 16	. . . . . . . . . . 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 233	. . . . . . . . . 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 2882	. . . . . . . . 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 2882	. . . . . . . 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 2467	. . . . . . . . 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 6862	. . . . . . . 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 196	. . . . . . 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 9117	. . . . . 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 9112	. . . . 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 14533	. . . 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 2555	. . 3 |- ( ph -> O e. U )
64		inss2 3724	. . . . 5 |- ( U i^i Cat ) C_ Cat
65	64, 13	sseldi 3507	. . . 4 |- ( ph -> X e. Cat )
66	5	oppccat 14994	. . . 4 |- ( X e. Cat -> O e. Cat )
67	65, 66	syl 16	. . 3 |- ( ph -> O e. Cat )
68	63, 67	elind 3693	. 2 |- ( ph -> O e. ( U i^i Cat ) )
69	68, 12	eleqtrrd 2558	1 |- ( ph -> O e. B )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   A.wral 2817   u. cun 3479   i^i cin 3480   C_ wss 3481   (/)c0 3790   ~Pcpw 4016   {csn 4033   <.cop 4039   U.cuni 4251   X. cxp 5003   `'ccnv 5004   dom cdm 5005   ran crn 5006   -->wf 5590   ` cfv 5594  (class class class)co 6295   |-> cmpt2 6297   omcom 6695   1stc1st 6793   2ndc2nd 6794  tpos ctpos 6966  WUnicwun 9090   1c1 9505   4c4 10599   5c5 10600  ;cdc 10988   ndxcnx 14503   sSet csts 14504   Basecbs 14506   Hom chom 14582  compcco 14583   Catccat 14935  oppCatcoppc 14983  CatCatccatc 15295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-tpos 6967  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-omul 7147  df-er 7323  df-ec 7325  df-qs 7329  df-map 7434  df-pm 7435  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-wun 9092  df-ni 9262  df-pli 9263  df-mi 9264  df-lti 9265  df-plpq 9298  df-mpq 9299  df-ltpq 9300  df-enq 9301  df-nq 9302  df-erq 9303  df-plq 9304  df-mq 9305  df-1nq 9306  df-rq 9307  df-ltnq 9308  df-np 9371  df-plp 9373  df-ltp 9375  df-enr 9445  df-nr 9446  df-c 9510  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-fz 11685  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-hom 14595  df-cco 14596  df-cat 14939  df-cid 14940  df-oppc 14984  df-catc 15296

This theorem is referenced by: (None)