funcid

Description: A functor maps each identity to the corresponding identity in the target category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	funcid.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	funcid.1	⊢ 1 = ( Id ‘ 𝐷 )
	funcid.i	⊢ 𝐼 = ( Id ‘ 𝐸 )
	funcid.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	funcid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	funcid	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funcid.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		funcid.1	⊢ 1 = ( Id ‘ 𝐷 )
3		funcid.i	⊢ 𝐼 = ( Id ‘ 𝐸 )
4		funcid.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		funcid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7	6 6	oveq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐺 𝑥 ) = ( 𝑋 𝐺 𝑋 ) )
8		fveq2	⊢ ( 𝑥 = 𝑋 → ( 1 ‘ 𝑥 ) = ( 1 ‘ 𝑋 ) )
9	7 8	fveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( ( 𝑋 𝐺 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) )
10		2fveq3	⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) )
11	9 10	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑋 𝐺 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
12		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
13		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
14		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
15		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
16		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
17		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
18	4 17	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
19		funcrcl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
20	18 19	syl	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
21	20	simpld	⊢ ( 𝜑 → 𝐷 ∈ Cat )
22	20	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
23	1 12 13 14 2 3 15 16 21 22	isfunc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐷 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
24	4 23	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( ( Hom ‘ 𝐷 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
25	24	simp3d	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
26		simpl	⊢ ( ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) → ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
27	26	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
28	25 27	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) )
29	11 28 5	rspcdva	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem funcid

Proof