cofurid

Description: The identity functor is a right identity for composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofulid.g	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofurid.1	⊢ 𝐼 = ( id_func ‘ 𝐶 )
Assertion	cofurid	⊢ ( 𝜑 → ( 𝐹 ∘_func 𝐼 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		cofulid.g	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		cofurid.1	⊢ 𝐼 = ( id_func ‘ 𝐶 )
3		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
4		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
6	5	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
7	2 3 6	idfu1st	⊢ ( 𝜑 → ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐶 ) ) )
8	7	coeq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐼 ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( I ↾ ( Base ‘ 𝐶 ) ) ) )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
11		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
12	10 1 11	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
13	3 9 12	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
14		fcoi1	⊢ ( ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) → ( ( 1^st ‘ 𝐹 ) ∘ ( I ↾ ( Base ‘ 𝐶 ) ) ) = ( 1^st ‘ 𝐹 ) )
15	13 14	syl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ∘ ( I ↾ ( Base ‘ 𝐶 ) ) ) = ( 1^st ‘ 𝐹 ) )
16	8 15	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐼 ) ) = ( 1^st ‘ 𝐹 ) )
17	7	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐶 ) ) )
18	17	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) = ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) )
19		fvresi	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) = 𝑥 )
20	19	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑥 ) = 𝑥 )
21	18 20	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) = 𝑥 )
22	17	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) = ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) )
23		fvresi	⊢ ( 𝑦 ∈ ( Base ‘ 𝐶 ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) = 𝑦 )
24	23	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( I ↾ ( Base ‘ 𝐶 ) ) ‘ 𝑦 ) = 𝑦 )
25	22 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) = 𝑦 )
26	21 25	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
27	6	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
28		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
29		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
30		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
31	2 3 27 28 29 30	idfu2nd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
32	26 31	coeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∘ ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) )
33		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
34	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
35	3 28 33 34 29 30	funcf2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
36		fcoi1	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∘ ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
37	35 36	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∘ ( I ↾ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
38	32 37	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
39	38	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
40	3 12	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
41		fnov	⊢ ( ( 2^nd ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
42	40 41	sylib	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
43	39 42	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) ) ) = ( 2^nd ‘ 𝐹 ) )
44	16 43	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) ) ) ⟩ = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
45	2	idfucl	⊢ ( 𝐶 ∈ Cat → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
46	6 45	syl	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐶 Func 𝐶 ) )
47	3 46 1	cofuval	⊢ ( 𝜑 → ( 𝐹 ∘_func 𝐼 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ 𝐼 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝐼 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐼 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐼 ) 𝑦 ) ) ) ⟩ )
48		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
49	10 1 48	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
50	44 47 49	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘_func 𝐼 ) = 𝐹 )

Metamath Proof Explorer

Theorem cofurid

Proof