Metamath Proof Explorer


Theorem oppccatid

Description: Lemma for oppccat . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 O = oppCat C
Assertion oppccatid C Cat O Cat Id O = Id C

Proof

Step Hyp Ref Expression
1 oppcbas.1 O = oppCat C
2 eqid Base C = Base C
3 1 2 oppcbas Base C = Base O
4 3 a1i C Cat Base C = Base O
5 eqidd C Cat Hom O = Hom O
6 eqidd C Cat comp O = comp O
7 1 fvexi O V
8 7 a1i C Cat O V
9 biid x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w
10 eqid Hom C = Hom C
11 eqid Id C = Id C
12 simpl C Cat y Base C C Cat
13 simpr C Cat y Base C y Base C
14 2 10 11 12 13 catidcl C Cat y Base C Id C y y Hom C y
15 10 1 oppchom y Hom O y = y Hom C y
16 14 15 eleqtrrdi C Cat y Base C Id C y y Hom O y
17 eqid comp C = comp C
18 simpr1l C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w x Base C
19 simpr1r C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w y Base C
20 2 17 1 18 19 19 oppcco C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w Id C y x y comp O y f = f y y comp C x Id C y
21 simpl C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w C Cat
22 simpr31 C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w f x Hom O y
23 10 1 oppchom x Hom O y = y Hom C x
24 22 23 eleqtrdi C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w f y Hom C x
25 2 10 11 21 19 17 18 24 catrid C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w f y y comp C x Id C y = f
26 20 25 eqtrd C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w Id C y x y comp O y f = f
27 simpr2l C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w z Base C
28 2 17 1 19 19 27 oppcco C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g y y comp O z Id C y = Id C y z y comp C y g
29 simpr32 C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g y Hom O z
30 10 1 oppchom y Hom O z = z Hom C y
31 29 30 eleqtrdi C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g z Hom C y
32 2 10 11 21 27 17 19 31 catlid C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w Id C y z y comp C y g = g
33 28 32 eqtrd C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g y y comp O z Id C y = g
34 2 17 1 18 19 27 oppcco C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g x y comp O z f = f z y comp C x g
35 2 10 17 21 27 19 18 31 24 catcocl C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w f z y comp C x g z Hom C x
36 34 35 eqeltrd C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g x y comp O z f z Hom C x
37 10 1 oppchom x Hom O z = z Hom C x
38 36 37 eleqtrrdi C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g x y comp O z f x Hom O z
39 simpr2r C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w w Base C
40 simpr33 C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h z Hom O w
41 10 1 oppchom z Hom O w = w Hom C z
42 40 41 eleqtrdi C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h w Hom C z
43 2 10 17 21 39 27 19 42 31 18 24 catass C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w f z y comp C x g w z comp C x h = f w y comp C x g w z comp C y h
44 2 17 1 18 27 39 oppcco C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h x z comp O w f z y comp C x g = f z y comp C x g w z comp C x h
45 2 17 1 18 19 39 oppcco C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g w z comp C y h x y comp O w f = f w y comp C x g w z comp C y h
46 43 44 45 3eqtr4rd C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w g w z comp C y h x y comp O w f = h x z comp O w f z y comp C x g
47 2 17 1 19 27 39 oppcco C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h y z comp O w g = g w z comp C y h
48 47 oveq1d C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h y z comp O w g x y comp O w f = g w z comp C y h x y comp O w f
49 34 oveq2d C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h x z comp O w g x y comp O z f = h x z comp O w f z y comp C x g
50 46 48 49 3eqtr4d C Cat x Base C y Base C z Base C w Base C f x Hom O y g y Hom O z h z Hom O w h y z comp O w g x y comp O w f = h x z comp O w g x y comp O z f
51 4 5 6 8 9 16 26 33 38 50 iscatd2 C Cat O Cat Id O = y Base C Id C y
52 2 11 cidfn C Cat Id C Fn Base C
53 dffn5 Id C Fn Base C Id C = y Base C Id C y
54 52 53 sylib C Cat Id C = y Base C Id C y
55 54 eqeq2d C Cat Id O = Id C Id O = y Base C Id C y
56 55 anbi2d C Cat O Cat Id O = Id C O Cat Id O = y Base C Id C y
57 51 56 mpbird C Cat O Cat Id O = Id C