fucidcl

Description: The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucidcl.q	$⊢ Q = C FuncCat D$
	fucidcl.n	$⊢ N = C Nat D$
	fucidcl.x	$⊢ \underset{˙}{1} = Id (D)$
	fucidcl.f	$⊢ φ \to F \in (C Func D)$
Assertion	fucidcl	$⊢ φ \to \underset{˙}{1} \circ 1^{st} (F) \in (F N F)$

Proof

Step	Hyp	Ref	Expression
1		fucidcl.q	$⊢ Q = C FuncCat D$
2		fucidcl.n	$⊢ N = C Nat D$
3		fucidcl.x	$⊢ \underset{˙}{1} = Id (D)$
4		fucidcl.f	$⊢ φ \to F \in (C Func D)$
5		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
6	4 5	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
7	6	simprd	$⊢ φ \to D \in Cat$
8		eqid	$⊢ {Base}_{D} = {Base}_{D}$
9	8 3	cidfn	$⊢ D \in Cat \to \underset{˙}{1} Fn {Base}_{D}$
10	7 9	syl	$⊢ φ \to \underset{˙}{1} Fn {Base}_{D}$
11		dffn2	$⊢ \underset{˙}{1} Fn {Base}_{D} \leftrightarrow \underset{˙}{1} : {Base}_{D} ⟶ V$
12	10 11	sylib	$⊢ φ \to \underset{˙}{1} : {Base}_{D} ⟶ V$
13		eqid	$⊢ {Base}_{C} = {Base}_{C}$
14		relfunc	$⊢ Rel (C Func D)$
15		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
16	14 4 15	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
17	13 8 16	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
18		fcompt	$⊢ (\underset{˙}{1} : {Base}_{D} ⟶ V \land 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}) \to \underset{˙}{1} \circ 1^{st} (F) = (x \in {Base}_{C} ⟼ \underset{˙}{1} (1^{st} (F) (x)))$
19	12 17 18	syl2anc	$⊢ φ \to \underset{˙}{1} \circ 1^{st} (F) = (x \in {Base}_{C} ⟼ \underset{˙}{1} (1^{st} (F) (x)))$
20		eqid	$⊢ Hom (D) = Hom (D)$
21	7	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
22	17	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
23	8 20 3 21 22	catidcl	$⊢ (φ \land x \in {Base}_{C}) \to \underset{˙}{1} (1^{st} (F) (x)) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (x))$
24	23	ralrimiva	$⊢ φ \to \forall x \in {Base}_{C} \underset{˙}{1} (1^{st} (F) (x)) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (x))$
25		fvex	$⊢ {Base}_{C} \in V$
26		mptelixpg	$⊢ {Base}_{C} \in V \to ((x \in {Base}_{C} ⟼ \underset{˙}{1} (1^{st} (F) (x))) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (F) (x)) \leftrightarrow \forall x \in {Base}_{C} \underset{˙}{1} (1^{st} (F) (x)) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (x)))$
27	25 26	ax-mp	$⊢ (x \in {Base}_{C} ⟼ \underset{˙}{1} (1^{st} (F) (x))) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (F) (x)) \leftrightarrow \forall x \in {Base}_{C} \underset{˙}{1} (1^{st} (F) (x)) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (x))$
28	24 27	sylibr	$⊢ φ \to (x \in {Base}_{C} ⟼ \underset{˙}{1} (1^{st} (F) (x))) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (F) (x))$
29	19 28	eqeltrd	$⊢ φ \to \underset{˙}{1} \circ 1^{st} (F) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (F) (x))$
30	7	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to D \in Cat$
31		simpr1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to x \in {Base}_{C}$
32	31 22	syldan	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) (x) \in {Base}_{D}$
33		eqid	$⊢ comp (D) = comp (D)$
34	17	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
35		simpr2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to y \in {Base}_{C}$
36	34 35	ffvelrnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) (y) \in {Base}_{D}$
37		eqid	$⊢ Hom (C) = Hom (C)$
38	16	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
39	13 37 20 38 31 35	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
40		simpr3	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to f \in (x Hom (C) y)$
41	39 40	ffvelrnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (F) y) (f) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (y))$
42	8 20 3 30 32 33 36 41	catlid	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to \underset{˙}{1} (1^{st} (F) (y)) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (F) y) (f)$
43	8 20 3 30 32 33 36 41	catrid	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) \underset{˙}{1} (1^{st} (F) (x)) = (x 2^{nd} (F) y) (f)$
44	42 43	eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to \underset{˙}{1} (1^{st} (F) (y)) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) \underset{˙}{1} (1^{st} (F) (x))$
45		fvco3	$⊢ (1^{st} (F) : {Base}_{C} ⟶ {Base}_{D} \land y \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (F)) (y) = \underset{˙}{1} (1^{st} (F) (y))$
46	34 35 45	syl2anc	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (\underset{˙}{1} \circ 1^{st} (F)) (y) = \underset{˙}{1} (1^{st} (F) (y))$
47	46	oveq1d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (\underset{˙}{1} \circ 1^{st} (F)) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f) = \underset{˙}{1} (1^{st} (F) (y)) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f)$
48		fvco3	$⊢ (1^{st} (F) : {Base}_{C} ⟶ {Base}_{D} \land x \in {Base}_{C}) \to (\underset{˙}{1} \circ 1^{st} (F)) (x) = \underset{˙}{1} (1^{st} (F) (x))$
49	34 31 48	syl2anc	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (\underset{˙}{1} \circ 1^{st} (F)) (x) = \underset{˙}{1} (1^{st} (F) (x))$
50	49	oveq2d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) (\underset{˙}{1} \circ 1^{st} (F)) (x) = (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) \underset{˙}{1} (1^{st} (F) (x))$
51	44 47 50	3eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (\underset{˙}{1} \circ 1^{st} (F)) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) (\underset{˙}{1} \circ 1^{st} (F)) (x)$
52	51	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall f \in (x Hom (C) y) (\underset{˙}{1} \circ 1^{st} (F)) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) (\underset{˙}{1} \circ 1^{st} (F)) (x)$
53	2 13 37 20 33 4 4	isnat2	$⊢ φ \to (\underset{˙}{1} \circ 1^{st} (F) \in (F N F) \leftrightarrow (\underset{˙}{1} \circ 1^{st} (F) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (F) (x)) \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall f \in (x Hom (C) y) (\underset{˙}{1} \circ 1^{st} (F)) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (F) y) (f) (⟨1^{st} (F) (x), 1^{st} (F) (x)⟩ comp (D) 1^{st} (F) (y)) (\underset{˙}{1} \circ 1^{st} (F)) (x)))$
54	29 52 53	mpbir2and	$⊢ φ \to \underset{˙}{1} \circ 1^{st} (F) \in (F N F)$

Metamath Proof Explorer

Theorem fucidcl

Proof