diag1a

Description: The constant functor of X . (Contributed by Zhi Wang, 19-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	diag1a	$⊢ φ \to K = ⟨B \times \{X\}, (y \in B, z \in B ⟼ (y J z) \times \{\underset{˙}{1} (X)\})⟩$

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	1 2 3 4 5 6 7 8 9	diag1	$⊢ φ \to K = ⟨(y \in B ⟼ X), (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))⟩$
11		fconstmpt	$⊢ B \times \{X\} = (y \in B ⟼ X)$
12		fconstmpt	$⊢ (y J z) \times \{\underset{˙}{1} (X)\} = (f \in (y J z) ⟼ \underset{˙}{1} (X))$
13	12	a1i	$⊢ (y \in B \land z \in B) \to (y J z) \times \{\underset{˙}{1} (X)\} = (f \in (y J z) ⟼ \underset{˙}{1} (X))$
14	13	mpoeq3ia	$⊢ (y \in B, z \in B ⟼ (y J z) \times \{\underset{˙}{1} (X)\}) = (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))$
15	11 14	opeq12i	$⊢ ⟨B \times \{X\}, (y \in B, z \in B ⟼ (y J z) \times \{\underset{˙}{1} (X)\})⟩ = ⟨(y \in B ⟼ X), (y \in B, z \in B ⟼ (f \in (y J z) ⟼ \underset{˙}{1} (X)))⟩$
16	10 15	eqtr4di	$⊢ φ \to K = ⟨B \times \{X\}, (y \in B, z \in B ⟼ (y J z) \times \{\underset{˙}{1} (X)\})⟩$

Metamath Proof Explorer