diag1

Description: The constant functor of X . (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	diag1.l	$⊢ L = C Δ_{func} D$
	diag1.c	$⊢ φ \to C \in Cat$
	diag1.d	$⊢ φ \to D \in Cat$
	diag1.a	$⊢ A = {Base}_{C}$
	diag1.x	$⊢ φ \to X \in A$
	diag1.k	$⊢ K = 1^{st} (L) (X)$
	diag1.b	$⊢ B = {Base}_{D}$
	diag1.j	$⊢ J = Hom (D)$
	diag1.i	$⊢ \underset{˙}{1} = Id (C)$
Assertion	diag1	$⊢ φ \to K = ⟨(y \in B ⟼ X), (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))⟩$

Proof

Step	Hyp	Ref	Expression
1		diag1.l	$⊢ L = C Δ_{func} D$
2		diag1.c	$⊢ φ \to C \in Cat$
3		diag1.d	$⊢ φ \to D \in Cat$
4		diag1.a	$⊢ A = {Base}_{C}$
5		diag1.x	$⊢ φ \to X \in A$
6		diag1.k	$⊢ K = 1^{st} (L) (X)$
7		diag1.b	$⊢ B = {Base}_{D}$
8		diag1.j	$⊢ J = Hom (D)$
9		diag1.i	$⊢ \underset{˙}{1} = Id (C)$
10		relfunc	$⊢ Rel (D Func C)$
11	1 2 3 4 5 6	diag1cl	$⊢ φ \to K \in (D Func C)$
12		1st2nd	$⊢ (Rel (D Func C) \land K \in (D Func C)) \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
13	10 11 12	sylancr	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
14		1st2ndbr	$⊢ (Rel (D Func C) \land K \in (D Func C)) \to 1^{st} (K) (D Func C) 2^{nd} (K)$
15	10 11 14	sylancr	$⊢ φ \to 1^{st} (K) (D Func C) 2^{nd} (K)$
16	7 4 15	funcf1	$⊢ φ \to 1^{st} (K) : B ⟶ A$
17	16	feqmptd	$⊢ φ \to 1^{st} (K) = (y \in B ⟼ 1^{st} (K) (y))$
18	2	adantr	$⊢ (φ \land y \in B) \to C \in Cat$
19	3	adantr	$⊢ (φ \land y \in B) \to D \in Cat$
20	5	adantr	$⊢ (φ \land y \in B) \to X \in A$
21		simpr	$⊢ (φ \land y \in B) \to y \in B$
22	1 18 19 4 20 6 7 21	diag11	$⊢ (φ \land y \in B) \to 1^{st} (K) (y) = X$
23	22	mpteq2dva	$⊢ φ \to (y \in B ⟼ 1^{st} (K) (y)) = (y \in B ⟼ X)$
24	17 23	eqtrd	$⊢ φ \to 1^{st} (K) = (y \in B ⟼ X)$
25	7 15	funcfn2	$⊢ φ \to 2^{nd} (K) Fn (B \times B)$
26		fnov	$⊢ 2^{nd} (K) Fn (B \times B) \leftrightarrow 2^{nd} (K) = (y \in B, z \in B ⟼ y 2^{nd} (K) z)$
27	25 26	sylib	$⊢ φ \to 2^{nd} (K) = (y \in B, z \in B ⟼ y 2^{nd} (K) z)$
28		eqid	$⊢ Hom (C) = Hom (C)$
29	15	3ad2ant1	$⊢ (φ \land y \in B \land z \in B) \to 1^{st} (K) (D Func C) 2^{nd} (K)$
30		simp2	$⊢ (φ \land y \in B \land z \in B) \to y \in B$
31		simp3	$⊢ (φ \land y \in B \land z \in B) \to z \in B$
32	7 8 28 29 30 31	funcf2	$⊢ (φ \land y \in B \land z \in B) \to (y 2^{nd} (K) z) : y J z ⟶ 1^{st} (K) (y) Hom (C) 1^{st} (K) (z)$
33	32	feqmptd	$⊢ (φ \land y \in B \land z \in B) \to y 2^{nd} (K) z = (f \in (y J z) ⟼ (y 2^{nd} (K) z) (f))$
34		simpl1	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to φ$
35	34 2	syl	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to C \in Cat$
36	34 3	syl	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to D \in Cat$
37	34 5	syl	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to X \in A$
38	30	adantr	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to y \in B$
39	31	adantr	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to z \in B$
40		simpr	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to f \in (y J z)$
41	1 35 36 4 37 6 7 38 8 9 39 40	diag12	$⊢ ((φ \land y \in B \land z \in B) \land f \in (y J z)) \to (y 2^{nd} (K) z) (f) = \underset{˙}{1} (X)$
42	41	mpteq2dva	$⊢ (φ \land y \in B \land z \in B) \to (f \in (y J z) ⟼ (y 2^{nd} (K) z) (f)) = (f \in (y J z) ⟼ \underset{˙}{1} (X))$
43	33 42	eqtrd	$⊢ (φ \land y \in B \land z \in B) \to y 2^{nd} (K) z = (f \in (y J z) ⟼ \underset{˙}{1} (X))$
44	43	mpoeq3dva	$⊢ φ \to (y \in B, z \in B ⟼ y 2^{nd} (K) z) = (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))$
45	27 44	eqtrd	$⊢ φ \to 2^{nd} (K) = (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))$
46	24 45	opeq12d	$⊢ φ \to ⟨1^{st} (K), 2^{nd} (K)⟩ = ⟨(y \in B ⟼ X), (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))⟩$
47	13 46	eqtrd	$⊢ φ \to K = ⟨(y \in B ⟼ X), (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))⟩$

Metamath Proof Explorer

Theorem diag1

Proof