Metamath Proof Explorer

Theorem catcoppccl

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

Ref Expression
Hypotheses 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 catcoppccl 
|- ( ph -> O e. B )

Proof

Step Hyp Ref Expression
1 catcoppccl.c 
 |-  C = ( CatCat ` U )
2 catcoppccl.b 
 |-  B = ( Base ` C )
3 catcoppccl.o 
 |-  O = ( oppCat ` X )
4 catcoppccl.1 
 |-  ( ph -> U e. WUni )
5 catcoppccl.2 
 |-  ( ph -> _om e. U )
6 catcoppccl.3 
 |-  ( ph -> X e. B )
7 eqid 
 |-  ( Base ` X ) = ( Base ` X )
8 eqid 
 |-  ( Hom ` X ) = ( Hom ` X )
9 eqid 
 |-  ( comp ` X ) = ( comp ` X )
10 7 8 9 3 oppcval 
 |-  ( 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 ) ) ) >. ) )
11 6 10 syl 
 |-  ( 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 ) ) ) >. ) )
12 1 2 4 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
13 6 12 eleqtrd 
 |-  ( ph -> X e. ( U i^i Cat ) )
14 13 elin1d 
 |-  ( ph -> X e. U )
15 df-hom 
 |-  Hom = Slot ; 1 4
16 4 5 wunndx 
 |-  ( ph -> ndx e. U )
17 15 4 16 wunstr 
 |-  ( ph -> ( Hom ` ndx ) e. U )
18 15 4 14 wunstr 
 |-  ( ph -> ( Hom ` X ) e. U )
19 4 18 wuntpos 
 |-  ( ph -> tpos ( Hom ` X ) e. U )
20 4 17 19 wunop 
 |-  ( ph -> <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. e. U )
21 4 14 20 wunsets 
 |-  ( ph -> ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) e. U )
22 df-cco 
 |-  comp = Slot ; 1 5
23 22 4 16 wunstr 
 |-  ( ph -> ( comp ` ndx ) e. U )
24 df-base 
 |-  Base = Slot 1
25 24 4 14 wunstr 
 |-  ( ph -> ( Base ` X ) e. U )
26 4 25 25 wunxp 
 |-  ( ph -> ( ( Base ` X ) X. ( Base ` X ) ) e. U )
27 4 26 25 wunxp 
 |-  ( ph -> ( ( ( Base ` X ) X. ( Base ` X ) ) X. ( Base ` X ) ) e. U )
28 22 4 14 wunstr 
 |-  ( ph -> ( comp ` X ) e. U )
29 4 28 wunrn 
 |-  ( ph -> ran ( comp ` X ) e. U )
30 4 29 wununi 
 |-  ( ph -> U. ran ( comp ` X ) e. U )
31 4 30 wundm 
 |-  ( ph -> dom U. ran ( comp ` X ) e. U )
32 4 31 wuncnv 
 |-  ( ph -> `' dom U. ran ( comp ` X ) e. U )
33 4 wun0 
 |-  ( ph -> (/) e. U )
34 4 33 wunsn 
 |-  ( ph -> { (/) } e. U )
35 4 32 34 wunun 
 |-  ( ph -> ( `' dom U. ran ( comp ` X ) u. { (/) } ) e. U )
36 4 30 wunrn 
 |-  ( ph -> ran U. ran ( comp ` X ) e. U )
37 4 35 36 wunxp 
 |-  ( ph -> ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) ) e. U )
38 4 37 wunpw 
 |-  ( ph -> ~P ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) ) e. U )
39 tposssxp 
 |-  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 ) ) )
40 ovssunirn 
 |-  ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ U. ran ( comp ` X )
41 dmss 
 |-  ( ( <. 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 ) )
42 40 41 ax-mp 
 |-  dom ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ dom U. ran ( comp ` X )
43 cnvss 
 |-  ( 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 ) )
44 unss1 
 |-  ( `' 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. { (/) } ) )
45 42 43 44 mp2b 
 |-  ( `' dom ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) u. { (/) } ) C_ ( `' dom U. ran ( comp ` X ) u. { (/) } )
46 40 rnssi 
 |-  ran ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ ran U. ran ( comp ` X )
47 xpss12 
 |-  ( ( ( `' 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 ) ) )
48 45 46 47 mp2an 
 |-  ( ( `' 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 ) )
49 39 48 sstri 
 |-  tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) )
50 elpw2g 
 |-  ( ( ( `' 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 ) ) ) )
51 37 50 syl 
 |-  ( 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 ) ) ) )
52 49 51 mpbiri 
 |-  ( ph -> tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) ) )
53 52 ralrimivw 
 |-  ( 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 ) ) )
54 53 ralrimivw 
 |-  ( 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 ) ) )
55 eqid 
 |-  ( 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 ) ) )
56 55 fmpo 
 |-  ( 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 ) ) )
57 54 56 sylib 
 |-  ( 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 ) ) )
58 4 27 38 57 wunf 
 |-  ( ph -> ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) ) e. U )
59 4 23 58 wunop 
 |-  ( ph -> <. ( comp ` ndx ) , ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) ) >. e. U )
60 4 21 59 wunsets 
 |-  ( 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 )
61 11 60 eqeltrd 
 |-  ( ph -> O e. U )
62 13 elin2d 
 |-  ( ph -> X e. Cat )
63 3 oppccat 
 |-  ( X e. Cat -> O e. Cat )
64 62 63 syl 
 |-  ( ph -> O e. Cat )
65 61 64 elind 
 |-  ( ph -> O e. ( U i^i Cat ) )
66 65 12 eleqtrrd 
 |-  ( ph -> O e. B )