diag2f1olem

	Ref	Expression
Hypotheses	diag2f1o.l	$⊢ L = C Δ_{func} D$
	diag2f1o.a	$⊢ A = {Base}_{C}$
	diag2f1o.h	$⊢ H = Hom (C)$
	diag2f1o.x	$⊢ φ \to X \in A$
	diag2f1o.y	$⊢ φ \to Y \in A$
	diag2f1o.n	$⊢ N = D Nat C$
	diag2f1o.d	No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
	diag2f1olem.m	$⊢ φ \to M \in (1^{st} (L) (X) N 1^{st} (L) (Y))$
	diag2f1olem.b	$⊢ B = {Base}_{D}$
	diag2f1olem.z	$⊢ φ \to Z \in B$
	diag2f1olem.f	$⊢ F = M (Z)$
Assertion	diag2f1olem	$⊢ φ \to (F \in (X H Y) \land M = (X 2^{nd} (L) Y) (F))$

Proof

Step	Hyp	Ref	Expression
1		diag2f1o.l	$⊢ L = C Δ_{func} D$
2		diag2f1o.a	$⊢ A = {Base}_{C}$
3		diag2f1o.h	$⊢ H = Hom (C)$
4		diag2f1o.x	$⊢ φ \to X \in A$
5		diag2f1o.y	$⊢ φ \to Y \in A$
6		diag2f1o.n	$⊢ N = D Nat C$
7		diag2f1o.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for \|- ( ph -> D e. TermCat ) with typecode \|-
8		diag2f1olem.m	$⊢ φ \to M \in (1^{st} (L) (X) N 1^{st} (L) (Y))$
9		diag2f1olem.b	$⊢ B = {Base}_{D}$
10		diag2f1olem.z	$⊢ φ \to Z \in B$
11		diag2f1olem.f	$⊢ F = M (Z)$
12	6 8	nat1st2nd	$⊢ φ \to M \in (⟨1^{st} (1^{st} (L) (X)), 2^{nd} (1^{st} (L) (X))⟩ N ⟨1^{st} (1^{st} (L) (Y)), 2^{nd} (1^{st} (L) (Y))⟩)$
13	6 12 9 3 10	natcl	$⊢ φ \to M (Z) \in (1^{st} (1^{st} (L) (X)) (Z) H 1^{st} (1^{st} (L) (Y)) (Z))$
14	6 12	natrcl2	$⊢ φ \to 1^{st} (1^{st} (L) (X)) (D Func C) 2^{nd} (1^{st} (L) (X))$
15	14	funcrcl3	$⊢ φ \to C \in Cat$
16	7	termccatd	$⊢ φ \to D \in Cat$
17		eqid	$⊢ 1^{st} (L) (X) = 1^{st} (L) (X)$
18	1 15 16 2 4 17 9 10	diag11	$⊢ φ \to 1^{st} (1^{st} (L) (X)) (Z) = X$
19		eqid	$⊢ 1^{st} (L) (Y) = 1^{st} (L) (Y)$
20	1 15 16 2 5 19 9 10	diag11	$⊢ φ \to 1^{st} (1^{st} (L) (Y)) (Z) = Y$
21	18 20	oveq12d	$⊢ φ \to 1^{st} (1^{st} (L) (X)) (Z) H 1^{st} (1^{st} (L) (Y)) (Z) = X H Y$
22	13 21	eleqtrd	$⊢ φ \to M (Z) \in (X H Y)$
23	11 22	eqeltrid	$⊢ φ \to F \in (X H Y)$
24	7 6 8 9 10 11	termcnatval	$⊢ φ \to M = \{⟨Z, F⟩\}$
25	1 2 9 3 15 16 4 5 23	diag2	$⊢ φ \to (X 2^{nd} (L) Y) (F) = B \times \{F\}$
26	7 9 10	termcbas2	$⊢ φ \to B = \{Z\}$
27	26	xpeq1d	$⊢ φ \to B \times \{F\} = \{Z\} \times \{F\}$
28		xpsng	$⊢ (Z \in B \land F \in (X H Y)) \to \{Z\} \times \{F\} = \{⟨Z, F⟩\}$
29	10 23 28	syl2anc	$⊢ φ \to \{Z\} \times \{F\} = \{⟨Z, F⟩\}$
30	25 27 29	3eqtrd	$⊢ φ \to (X 2^{nd} (L) Y) (F) = \{⟨Z, F⟩\}$
31	24 30	eqtr4d	$⊢ φ \to M = (X 2^{nd} (L) Y) (F)$
32	23 31	jca	$⊢ φ \to (F \in (X H Y) \land M = (X 2^{nd} (L) Y) (F))$

Metamath Proof Explorer

Theorem diag2f1olem

Proof