Metamath Proof Explorer

Theorem oppccatid

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

Ref Expression
Hypothesis oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion oppccatid ( 𝐶 ∈ Cat → ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 oppcbas.1 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3 1 2 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
4 3 a1i ⊢ ( 𝐶 ∈ Cat → ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 ) )
5 eqidd ⊢ ( 𝐶 ∈ Cat → ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 ) )
6 eqidd ⊢ ( 𝐶 ∈ Cat → ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 ) )
7 1 fvexi ⊢ 𝑂 ∈ V
8 7 a1i ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ V )
9 biid ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) )
10 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
13 simpr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
14 2 10 11 12 13 catidcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 ) )
15 10 1 oppchom ⊢ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑦 )
16 14 15 eleqtrrdi ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑦 ) )
17 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
18 simpr1l ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
19 simpr1r ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
20 2 17 1 18 19 19 oppcco ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑦 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) )
21 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝐶 ∈ Cat )
22 simpr31 ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) )
23 10 1 oppchom ⊢ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
24 22 23 eleqtrdi ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
25 2 10 11 21 19 17 18 24 catrid ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑓 ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) = 𝑓 )
26 20 25 eqtrd ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑦 ) 𝑓 ) = 𝑓 )
27 simpr2l ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
28 2 17 1 19 19 27 oppcco ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) )
29 simpr32 ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) )
30 10 1 oppchom ⊢ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑦 )
31 29 30 eleqtrdi ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑦 ) )
32 2 10 11 21 27 17 19 31 catlid ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑔 ) = 𝑔 )
33 28 32 eqtrd ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) = 𝑔 )
34 2 17 1 18 19 27 oppcco ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) )
35 2 10 17 21 27 19 18 31 24 catcocl ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑥 ) )
36 34 35 eqeltrd ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑥 ) )
37 10 1 oppchom ⊢ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑥 )
38 36 37 eleqtrrdi ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑧 ) )
39 simpr2r ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
40 simpr33 ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) )
41 10 1 oppchom ⊢ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) = ( 𝑤 ( Hom ‘ 𝐶 ) 𝑧 )
42 40 41 eleqtrdi ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ℎ ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑧 ) )
43 2 10 17 21 39 27 19 42 31 18 24 catass ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ℎ ) = ( 𝑓 ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ℎ ) ) )
44 2 17 1 18 27 39 oppcco ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ) = ( ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ℎ ) )
45 2 17 1 18 19 39 oppcco ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( 𝑔 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ℎ ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑓 ) = ( 𝑓 ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ( 𝑔 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ℎ ) ) )
46 43 44 45 3eqtr4rd ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( 𝑔 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ℎ ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑓 ) = ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ) )
47 2 17 1 19 27 39 oppcco ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑔 ) = ( 𝑔 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ℎ ) )
48 47 oveq1d ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑓 ) = ( ( 𝑔 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ℎ ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑓 ) )
49 34 oveq2d ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) = ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) ( 𝑓 ( ⟨ 𝑧 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑔 ) ) )
50 46 48 49 3eqtr4d ⊢ ( ( 𝐶 ∈ Cat ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑂 ) 𝑧 ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ) → ( ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑓 ) = ( ℎ ( ⟨ 𝑥 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑂 ) 𝑧 ) 𝑓 ) ) )
51 4 5 6 8 9 16 26 33 38 50 iscatd2 ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) ) )
52 2 11 cidfn ⊢ ( 𝐶 ∈ Cat → ( Id ‘ 𝐶 ) Fn ( Base ‘ 𝐶 ) )
53 dffn5 ⊢ ( ( Id ‘ 𝐶 ) Fn ( Base ‘ 𝐶 ) ↔ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) )
54 52 53 sylib ⊢ ( 𝐶 ∈ Cat → ( Id ‘ 𝐶 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) )
55 54 eqeq2d ⊢ ( 𝐶 ∈ Cat → ( ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) ↔ ( Id ‘ 𝑂 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) ) )
56 55 anbi2d ⊢ ( 𝐶 ∈ Cat → ( ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) ) ↔ ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑦 ) ) ) ) )
57 51 56 mpbird ⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) ) )