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 φ U WUni
catcoppccl.2 φ ω U
catcoppccl.3 φ X B
Assertion catcoppcclOLD φ O 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 φ U WUni
5 catcoppccl.2 φ ω U
6 catcoppccl.3 φ X 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 B O = X sSet Hom ndx tpos Hom X sSet comp ndx x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x
11 6 10 syl φ O = X sSet Hom ndx tpos Hom X sSet comp ndx x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x
12 1 2 4 catcbas φ B = U Cat
13 6 12 eleqtrd φ X U Cat
14 13 elin1d φ X U
15 df-hom Hom = Slot 14
16 4 5 wunndx φ ndx U
17 15 4 16 wunstr φ Hom ndx U
18 15 4 14 wunstr φ Hom X U
19 4 18 wuntpos φ tpos Hom X U
20 4 17 19 wunop φ Hom ndx tpos Hom X U
21 4 14 20 wunsets φ X sSet Hom ndx tpos Hom X U
22 df-cco comp = Slot 15
23 22 4 16 wunstr φ comp ndx U
24 df-base Base = Slot 1
25 24 4 14 wunstr φ Base X U
26 4 25 25 wunxp φ Base X × Base X U
27 4 26 25 wunxp φ Base X × Base X × Base X U
28 22 4 14 wunstr φ comp X U
29 4 28 wunrn φ ran comp X U
30 4 29 wununi φ ran comp X U
31 4 30 wundm φ dom ran comp X U
32 4 31 wuncnv φ dom ran comp X -1 U
33 4 wun0 φ U
34 4 33 wunsn φ U
35 4 32 34 wunun φ dom ran comp X -1 U
36 4 30 wunrn φ ran ran comp X U
37 4 35 36 wunxp φ dom ran comp X -1 × ran ran comp X U
38 4 37 wunpw φ 𝒫 dom ran comp X -1 × ran ran comp X U
39 tposssxp tpos y 2 nd x comp X 1 st x dom y 2 nd x comp X 1 st x -1 × ran y 2 nd x comp X 1 st x
40 ovssunirn y 2 nd x comp X 1 st x ran comp X
41 dmss y 2 nd x comp X 1 st x ran comp X dom y 2 nd x comp X 1 st x dom ran comp X
42 40 41 ax-mp dom y 2 nd x comp X 1 st x dom ran comp X
43 cnvss dom y 2 nd x comp X 1 st x dom ran comp X dom y 2 nd x comp X 1 st x -1 dom ran comp X -1
44 unss1 dom y 2 nd x comp X 1 st x -1 dom ran comp X -1 dom y 2 nd x comp X 1 st x -1 dom ran comp X -1
45 42 43 44 mp2b dom y 2 nd x comp X 1 st x -1 dom ran comp X -1
46 40 rnssi ran y 2 nd x comp X 1 st x ran ran comp X
47 xpss12 dom y 2 nd x comp X 1 st x -1 dom ran comp X -1 ran y 2 nd x comp X 1 st x ran ran comp X dom y 2 nd x comp X 1 st x -1 × ran y 2 nd x comp X 1 st x dom ran comp X -1 × ran ran comp X
48 45 46 47 mp2an dom y 2 nd x comp X 1 st x -1 × ran y 2 nd x comp X 1 st x dom ran comp X -1 × ran ran comp X
49 39 48 sstri tpos y 2 nd x comp X 1 st x dom ran comp X -1 × ran ran comp X
50 elpw2g dom ran comp X -1 × ran ran comp X U tpos y 2 nd x comp X 1 st x 𝒫 dom ran comp X -1 × ran ran comp X tpos y 2 nd x comp X 1 st x dom ran comp X -1 × ran ran comp X
51 37 50 syl φ tpos y 2 nd x comp X 1 st x 𝒫 dom ran comp X -1 × ran ran comp X tpos y 2 nd x comp X 1 st x dom ran comp X -1 × ran ran comp X
52 49 51 mpbiri φ tpos y 2 nd x comp X 1 st x 𝒫 dom ran comp X -1 × ran ran comp X
53 52 ralrimivw φ y Base X tpos y 2 nd x comp X 1 st x 𝒫 dom ran comp X -1 × ran ran comp X
54 53 ralrimivw φ x Base X × Base X y Base X tpos y 2 nd x comp X 1 st x 𝒫 dom ran comp X -1 × ran ran comp X
55 eqid x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x = x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x
56 55 fmpo x Base X × Base X y Base X tpos y 2 nd x comp X 1 st x 𝒫 dom ran comp X -1 × ran ran comp X x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x : Base X × Base X × Base X 𝒫 dom ran comp X -1 × ran ran comp X
57 54 56 sylib φ x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x : Base X × Base X × Base X 𝒫 dom ran comp X -1 × ran ran comp X
58 4 27 38 57 wunf φ x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x U
59 4 23 58 wunop φ comp ndx x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x U
60 4 21 59 wunsets φ X sSet Hom ndx tpos Hom X sSet comp ndx x Base X × Base X , y Base X tpos y 2 nd x comp X 1 st x U
61 11 60 eqeltrd φ O U
62 13 elin2d φ X Cat
63 3 oppccat X Cat O Cat
64 62 63 syl φ O Cat
65 61 64 elind φ O U Cat
66 65 12 eleqtrrd φ O B