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) (Proof shortened by AV, 13-Oct-2024)

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 6 catcbascl 
 |-  ( ph -> X e. U )
13 homid 
 |-  Hom = Slot ( Hom ` ndx )
14 4 5 wunndx 
 |-  ( ph -> ndx e. U )
15 13 4 14 wunstr 
 |-  ( ph -> ( Hom ` ndx ) e. U )
16 1 2 4 6 catchomcl 
 |-  ( ph -> ( Hom ` X ) e. U )
17 4 16 wuntpos 
 |-  ( ph -> tpos ( Hom ` X ) e. U )
18 4 15 17 wunop 
 |-  ( ph -> <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. e. U )
19 4 12 18 wunsets 
 |-  ( ph -> ( X sSet <. ( Hom ` ndx ) , tpos ( Hom ` X ) >. ) e. U )
20 ccoid 
 |-  comp = Slot ( comp ` ndx )
21 20 4 14 wunstr 
 |-  ( ph -> ( comp ` ndx ) e. U )
22 1 2 4 6 catcbaselcl 
 |-  ( ph -> ( Base ` X ) e. U )
23 4 22 22 wunxp 
 |-  ( ph -> ( ( Base ` X ) X. ( Base ` X ) ) e. U )
24 4 23 22 wunxp 
 |-  ( ph -> ( ( ( Base ` X ) X. ( Base ` X ) ) X. ( Base ` X ) ) e. U )
25 1 2 4 6 catcccocl 
 |-  ( ph -> ( comp ` X ) e. U )
26 4 25 wunrn 
 |-  ( ph -> ran ( comp ` X ) e. U )
27 4 26 wununi 
 |-  ( ph -> U. ran ( comp ` X ) e. U )
28 4 27 wundm 
 |-  ( ph -> dom U. ran ( comp ` X ) e. U )
29 4 28 wuncnv 
 |-  ( ph -> `' dom U. ran ( comp ` X ) e. U )
30 4 wun0 
 |-  ( ph -> (/) e. U )
31 4 30 wunsn 
 |-  ( ph -> { (/) } e. U )
32 4 29 31 wunun 
 |-  ( ph -> ( `' dom U. ran ( comp ` X ) u. { (/) } ) e. U )
33 4 27 wunrn 
 |-  ( ph -> ran U. ran ( comp ` X ) e. U )
34 4 32 33 wunxp 
 |-  ( ph -> ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) ) e. U )
35 4 34 wunpw 
 |-  ( ph -> ~P ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) ) e. U )
36 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 ) ) )
37 ovssunirn 
 |-  ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ U. ran ( comp ` X )
38 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 ) )
39 37 38 ax-mp 
 |-  dom ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ dom U. ran ( comp ` X )
40 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 ) )
41 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. { (/) } ) )
42 39 40 41 mp2b 
 |-  ( `' dom ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) u. { (/) } ) C_ ( `' dom U. ran ( comp ` X ) u. { (/) } )
43 37 rnssi 
 |-  ran ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ ran U. ran ( comp ` X )
44 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 ) ) )
45 42 43 44 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 ) )
46 36 45 sstri 
 |-  tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) C_ ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) )
47 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 ) ) ) )
48 34 47 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 ) ) ) )
49 46 48 mpbiri 
 |-  ( ph -> tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) e. ~P ( ( `' dom U. ran ( comp ` X ) u. { (/) } ) X. ran U. ran ( comp ` X ) ) )
50 49 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 ) ) )
51 50 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 ) ) )
52 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 ) ) )
53 52 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 ) ) )
54 51 53 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 ) ) )
55 4 24 35 54 wunf 
 |-  ( ph -> ( x e. ( ( Base ` X ) X. ( Base ` X ) ) , y e. ( Base ` X ) |-> tpos ( <. y , ( 2nd ` x ) >. ( comp ` X ) ( 1st ` x ) ) ) e. U )
56 4 21 55 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 )
57 4 19 56 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 )
58 11 57 eqeltrd 
 |-  ( ph -> O e. U )
59 1 2 4 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
60 6 59 eleqtrd 
 |-  ( ph -> X e. ( U i^i Cat ) )
61 60 elin2d 
 |-  ( ph -> X e. Cat )
62 3 oppccat 
 |-  ( X e. Cat -> O e. Cat )
63 61 62 syl 
 |-  ( ph -> O e. Cat )
64 58 63 elind 
 |-  ( ph -> O e. ( U i^i Cat ) )
65 64 59 eleqtrrd 
 |-  ( ph -> O e. B )