Metamath Proof Explorer


Theorem 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 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐷 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( 1𝑥 ) ) = ( 𝐼 ‘ ( 𝐹𝑥 ) ) ∧ ∀ 𝑦𝐵𝑧𝐵𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹𝑥 ) , ( 𝐹𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
24 4 23 mpbid ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2nd𝑧 ) ) ) ↑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𝑋 ) ) = ( 𝐼 ‘ ( 𝐹𝑋 ) ) )