Metamath Proof Explorer


Theorem catcoppcclOLD

Description: Obsolete proof of catcoppccl as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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 catcoppcclOLD
|- ( 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 )