Definition df-oppc

Description: Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of Adamek p. 25. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	df-oppc	⊢ oppCat = ( 𝑓 ∈ V ↦ ( ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coppc	⊢ oppCat
1		vf	⊢ 𝑓
2		cvv	⊢ V
3	1	cv	⊢ 𝑓
4		csts	⊢ sSet
5		chom	⊢ Hom
6		cnx	⊢ ndx
7	6 5	cfv	⊢ ( Hom ‘ ndx )
8	3 5	cfv	⊢ ( Hom ‘ 𝑓 )
9	8	ctpos	⊢ tpos ( Hom ‘ 𝑓 )
10	7 9	cop	⊢ ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩
11	3 10 4	co	⊢ ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ )
12		cco	⊢ comp
13	6 12	cfv	⊢ ( comp ‘ ndx )
14		vu	⊢ 𝑢
15		cbs	⊢ Base
16	3 15	cfv	⊢ ( Base ‘ 𝑓 )
17	16 16	cxp	⊢ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) )
18		vz	⊢ 𝑧
19	18	cv	⊢ 𝑧
20		c2nd	⊢ 2nd
21	14	cv	⊢ 𝑢
22	21 20	cfv	⊢ ( 2nd ‘ 𝑢 )
23	19 22	cop	⊢ ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩
24	3 12	cfv	⊢ ( comp ‘ 𝑓 )
25		c1st	⊢ 1st
26	21 25	cfv	⊢ ( 1st ‘ 𝑢 )
27	23 26 24	co	⊢ ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) )
28	27	ctpos	⊢ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) )
29	14 18 17 16 28	cmpo	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) )
30	13 29	cop	⊢ ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩
31	11 30 4	co	⊢ ( ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩ )
32	1 2 31	cmpt	⊢ ( 𝑓 ∈ V ↦ ( ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )
33	0 32	wceq	⊢ oppCat = ( 𝑓 ∈ V ↦ ( ( 𝑓 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑓 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑢 ∈ ( ( Base ‘ 𝑓 ) × ( Base ‘ 𝑓 ) ) , 𝑧 ∈ ( Base ‘ 𝑓 ) ↦ tpos ( ⟨ 𝑧 , ( 2nd ‘ 𝑢 ) ⟩ ( comp ‘ 𝑓 ) ( 1st ‘ 𝑢 ) ) ) ⟩ ) )