oppfdiag

Description: A diagonal functor for opposite categories is the opposite functor of the diagonal functor for original categories post-composed by an isomorphism ( fucoppc ). (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppfdiag.o	$⊢ O = oppCat (C)$
	oppfdiag.p	$⊢ P = oppCat (D)$
	oppfdiag.l	$⊢ L = C Δ_{func} D$
	oppfdiag.c	$⊢ φ \to C \in Cat$
	oppfdiag.d	$⊢ φ \to D \in Cat$
	oppfdiag.f	No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( D Func C ) ) ) with typecode \|-
	oppfdiag.n	$⊢ N = D Nat C$
	oppfdiag.g	$⊢ φ \to G = (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n N m)})$
Assertion	oppfdiag	Could not format assertion : No typesetting found for \|- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	$⊢ O = oppCat (C)$
2		oppfdiag.p	$⊢ P = oppCat (D)$
3		oppfdiag.l	$⊢ L = C Δ_{func} D$
4		oppfdiag.c	$⊢ φ \to C \in Cat$
5		oppfdiag.d	$⊢ φ \to D \in Cat$
6		oppfdiag.f	Could not format ( ph -> F = ( oppFunc \|` ( D Func C ) ) ) : No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( D Func C ) ) ) with typecode \|-
7		oppfdiag.n	$⊢ N = D Nat C$
8		oppfdiag.g	$⊢ φ \to G = (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n N m)})$
9		eqid	$⊢ {Base}_{C} = {Base}_{C}$
10	1 9	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
11		eqid	$⊢ P FuncCat O = P FuncCat O$
12	11	fucbas	$⊢ P Func O = {Base}_{(P FuncCat O)}$
13		eqid	$⊢ oppCat (D FuncCat C) = oppCat (D FuncCat C)$
14		eqid	$⊢ D FuncCat C = D FuncCat C$
15	3 4 5 14	diagcl	$⊢ φ \to L \in (C Func (D FuncCat C))$
16	1 13 15	oppfoppc2	Could not format ( ph -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode \|-
17	2 1 14 13 11 7 6 8 5 4	fucoppcfunc	$⊢ φ \to F (oppCat (D FuncCat C) Func (P FuncCat O)) G$
18		df-br	$⊢ F (oppCat (D FuncCat C) Func (P FuncCat O)) G \leftrightarrow ⟨F, G⟩ \in (oppCat (D FuncCat C) Func (P FuncCat O))$
19	17 18	sylib	$⊢ φ \to ⟨F, G⟩ \in (oppCat (D FuncCat C) Func (P FuncCat O))$
20	16 19	cofucl	Could not format ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) : No typesetting found for \|- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) with typecode \|-
21	20	func1st2nd	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) with typecode \|-
22	10 12 21	funcf1	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) : ( Base ` C ) --> ( P Func O ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) : ( Base ` C ) --> ( P Func O ) ) with typecode \|-
23	22	ffnd	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( Base ` C ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( Base ` C ) ) with typecode \|-
24		eqid	$⊢ O Δ_{func} P = O Δ_{func} P$
25	1	oppccat	$⊢ C \in Cat \to O \in Cat$
26	4 25	syl	$⊢ φ \to O \in Cat$
27	2	oppccat	$⊢ D \in Cat \to P \in Cat$
28	5 27	syl	$⊢ φ \to P \in Cat$
29	24 26 28 11	diagcl	$⊢ φ \to O Δ_{func} P \in (O Func (P FuncCat O))$
30	29	func1st2nd	$⊢ φ \to 1^{st} (O Δ_{func} P) (O Func (P FuncCat O)) 2^{nd} (O Δ_{func} P)$
31	10 12 30	funcf1	$⊢ φ \to 1^{st} (O Δ_{func} P) : {Base}_{C} ⟶ P Func O$
32	31	ffnd	$⊢ φ \to 1^{st} (O Δ_{func} P) Fn {Base}_{C}$
33	16	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode \|-
34	19	adantr	$⊢ (φ \land x \in {Base}_{C}) \to ⟨F, G⟩ \in (oppCat (D FuncCat C) Func (P FuncCat O))$
35		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
36	10 33 34 35	cofu1	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) ) with typecode \|-
37	17	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
38	15	oppf1	Could not format ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) ) with typecode \|-
39	38	fveq1d	Could not format ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` x ) = ( ( 1st ` L ) ` x ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` x ) = ( ( 1st ` L ) ` x ) ) with typecode \|-
40	37 39	fveq12d	Could not format ( ph -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) with typecode \|-
41	40	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) ) with typecode \|-
42	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
43	5	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
44	6	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> F = ( oppFunc \|` ( D Func C ) ) ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> F = ( oppFunc \|` ( D Func C ) ) ) with typecode \|-
45	1 2 3 42 43 44 9 35	oppfdiag1	$⊢ (φ \land x \in {Base}_{C}) \to F (1^{st} (L) (x)) = 1^{st} (O Δ_{func} P) (x)$
46	36 41 45	3eqtrd	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) ) with typecode \|-
47	23 32 46	eqfnfvd	Could not format ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 1st ` ( O DiagFunc P ) ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 1st ` ( O DiagFunc P ) ) ) with typecode \|-
48	10 21	funcfn2	Could not format ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) : No typesetting found for \|- ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) with typecode \|-
49	10 30	funcfn2	$⊢ φ \to 2^{nd} (O Δ_{func} P) Fn ({Base}_{C} \times {Base}_{C})$
50		eqid	$⊢ Hom (C) = Hom (C)$
51	50 1	oppchom	$⊢ x Hom (O) y = y Hom (C) x$
52	51	a1i	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x Hom (O) y = y Hom (C) x$
53		eqid	$⊢ Hom (O) = Hom (O)$
54		eqid	$⊢ P Nat O = P Nat O$
55	11 54	fuchom	$⊢ P Nat O = Hom (P FuncCat O)$
56	21	adantr	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) : No typesetting found for \|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ) with typecode \|-
57		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
58		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
59	10 53 55 56 57 58	funcf2	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( x ( Hom ` O ) y ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) : No typesetting found for \|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( x ( Hom ` O ) y ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) with typecode \|-
60	52 59	feq2dd	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( y ( Hom ` C ) x ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) : No typesetting found for \|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( y ( Hom ` C ) x ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) ) with typecode \|-
61	60	ffnd	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) Fn ( y ( Hom ` C ) x ) ) : No typesetting found for \|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) Fn ( y ( Hom ` C ) x ) ) with typecode \|-
62	30	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (O Δ_{func} P) (O Func (P FuncCat O)) 2^{nd} (O Δ_{func} P)$
63	10 53 55 62 57 58	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (O Δ_{func} P) y) : x Hom (O) y ⟶ 1^{st} (O Δ_{func} P) (x) (P Nat O) 1^{st} (O Δ_{func} P) (y)$
64	52 63	feq2dd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (O Δ_{func} P) y) : y Hom (C) x ⟶ 1^{st} (O Δ_{func} P) (x) (P Nat O) 1^{st} (O Δ_{func} P) (y)$
65	64	ffnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (O Δ_{func} P) y) Fn (y Hom (C) x)$
66	16	ad2antrr	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) ) with typecode \|-
67	19	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to ⟨F, G⟩ \in (oppCat (D FuncCat C) Func (P FuncCat O))$
68	57	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to x \in {Base}_{C}$
69	58	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to y \in {Base}_{C}$
70		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to f \in (y Hom (C) x)$
71	70 51	eleqtrrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to f \in (x Hom (O) y)$
72	10 66 67 68 69 53 71	cofu2	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) ) with typecode \|-
73	17	func2nd	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
74	38	fveq1d	Could not format ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` y ) = ( ( 1st ` L ) ` y ) ) : No typesetting found for \|- ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` y ) = ( ( 1st ` L ) ` y ) ) with typecode \|-
75	73 39 74	oveq123d	Could not format ( ph -> ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) = ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ) : No typesetting found for \|- ( ph -> ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) = ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ) with typecode \|-
76	15	oppf2	Could not format ( ph -> ( x ( 2nd ` ( oppFunc ` L ) ) y ) = ( y ( 2nd ` L ) x ) ) : No typesetting found for \|- ( ph -> ( x ( 2nd ` ( oppFunc ` L ) ) y ) = ( y ( 2nd ` L ) x ) ) with typecode \|-
77	76	fveq1d	Could not format ( ph -> ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) = ( ( y ( 2nd ` L ) x ) ` f ) ) : No typesetting found for \|- ( ph -> ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) = ( ( y ( 2nd ` L ) x ) ` f ) ) with typecode \|-
78	75 77	fveq12d	Could not format ( ph -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) : No typesetting found for \|- ( ph -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) with typecode \|-
79	78	ad2antrr	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) ) with typecode \|-
80	8	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to G = (m \in (D Func C), n \in (D Func C) ⟼ {I ↾}_{(n N m)})$
81	4	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to C \in Cat$
82	5	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to D \in Cat$
83		eqid	$⊢ 1^{st} (L) (x) = 1^{st} (L) (x)$
84	3 81 82 9 68 83	diag1cl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to 1^{st} (L) (x) \in (D Func C)$
85		eqid	$⊢ 1^{st} (L) (y) = 1^{st} (L) (y)$
86	3 81 82 9 69 85	diag1cl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to 1^{st} (L) (y) \in (D Func C)$
87		eqid	$⊢ {Base}_{D} = {Base}_{D}$
88	3 9 87 50 81 82 69 68 70	diag2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to (y 2^{nd} (L) x) (f) = {Base}_{D} \times \{f\}$
89	3 9 87 50 81 82 69 68 70 7	diag2cl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to {Base}_{D} \times \{f\} \in (1^{st} (L) (y) N 1^{st} (L) (x))$
90	80 84 86 88 89	opf2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to (1^{st} (L) (x) G 1^{st} (L) (y)) ((y 2^{nd} (L) x) (f)) = {Base}_{D} \times \{f\}$
91	72 79 90	3eqtrd	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( Base ` D ) X. { f } ) ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( Base ` D ) X. { f } ) ) with typecode \|-
92	2 87	oppcbas	$⊢ {Base}_{D} = {Base}_{P}$
93	81 25	syl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to O \in Cat$
94	82 27	syl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to P \in Cat$
95	24 10 92 53 93 94 68 69 71	diag2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (y Hom (C) x)) \to (x 2^{nd} (O Δ_{func} P) y) (f) = {Base}_{D} \times \{f\}$
96	91 95	eqtr4d	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( O DiagFunc P ) ) y ) ` f ) ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( O DiagFunc P ) ) y ) ` f ) ) with typecode \|-
97	61 65 96	eqfnfvd	Could not format ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) = ( x ( 2nd ` ( O DiagFunc P ) ) y ) ) : No typesetting found for \|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) = ( x ( 2nd ` ( O DiagFunc P ) ) y ) ) with typecode \|-
98	48 49 97	eqfnovd	Could not format ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 2nd ` ( O DiagFunc P ) ) ) : No typesetting found for \|- ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 2nd ` ( O DiagFunc P ) ) ) with typecode \|-
99	47 98	opeq12d	Could not format ( ph -> <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ) : No typesetting found for \|- ( ph -> <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. ) with typecode \|-
100		relfunc	$⊢ Rel (O Func (P FuncCat O))$
101		1st2nd	Could not format ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) : No typesetting found for \|- ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) with typecode \|-
102	100 20 101	sylancr	Could not format ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) : No typesetting found for \|- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. ) with typecode \|-
103		1st2nd	$⊢ (Rel (O Func (P FuncCat O)) \land O Δ_{func} P \in (O Func (P FuncCat O))) \to O Δ_{func} P = ⟨1^{st} (O Δ_{func} P), 2^{nd} (O Δ_{func} P)⟩$
104	100 29 103	sylancr	$⊢ φ \to O Δ_{func} P = ⟨1^{st} (O Δ_{func} P), 2^{nd} (O Δ_{func} P)⟩$
105	99 102 104	3eqtr4d	Could not format ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) ) : No typesetting found for \|- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) ) with typecode \|-

Metamath Proof Explorer

Theorem oppfdiag

Proof