This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imaid

Description: An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
imaid.i ⊢ 𝐼 = ( Id ‘ 𝐸 )
imaid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion imaid ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝑋 𝐾 𝑋 ) )

Proof

Step Hyp Ref Expression
1 imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2 imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4 imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 imaid.i ⊢ 𝐼 = ( Id ‘ 𝐸 )
6 imaid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7 6 1 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 “ 𝐴 ) )
8 inisegn0a ⊢ ( 𝑋 ∈ ( 𝐹 “ 𝐴 ) → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ∅ )
9 7 8 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑋 } ) ≠ ∅ )
10 n0 ⊢ ( ( ◡ 𝐹 “ { 𝑋 } ) ≠ ∅ ↔ ∃ 𝑚 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) )
11 9 10 sylib ⊢ ( 𝜑 → ∃ 𝑚 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) )
12 fveq2 ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑚 ⟩ ) )
13 df-ov ⊢ ( 𝑚 𝐺 𝑚 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑚 ⟩ )
14 12 13 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝑚 𝐺 𝑚 ) )
15 fveq2 ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑚 ⟩ ) )
16 df-ov ⊢ ( 𝑚 𝐻 𝑚 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑚 ⟩ )
17 15 16 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝑚 𝐻 𝑚 ) )
18 14 17 imaeq12d ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
19 18 eleq2d ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑚 ⟩ → ( ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ↔ ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) ) )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) )
21 20 20 opelxpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ⟨ 𝑚 , 𝑚 ⟩ ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) )
22 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
23 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
25 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
26 22 25 4 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
27 26 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐷 ) )
28 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐷 ) → ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ↔ ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑋 ) ) )
29 27 28 syl ⊢ ( 𝜑 → ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ↔ ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑋 ) ) )
30 29 biimpa ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑋 ) )
31 30 simpld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝑚 ∈ ( Base ‘ 𝐷 ) )
32 22 23 5 24 31 funcid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑚 ) ) )
33 30 simprd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑚 ) = 𝑋 )
34 33 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 𝐼 ‘ 𝑋 ) )
35 32 34 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) = ( 𝐼 ‘ 𝑋 ) )
36 24 funcrcl2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → 𝐷 ∈ Cat )
37 22 2 23 36 31 catidcl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ∈ ( 𝑚 𝐻 𝑚 ) )
38 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
39 22 2 38 24 31 31 funcf2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝑚 𝐺 𝑚 ) : ( 𝑚 𝐻 𝑚 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑚 ) ) )
40 39 funfvima2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) ∧ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ∈ ( 𝑚 𝐻 𝑚 ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
41 37 40 mpdan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( ( 𝑚 𝐺 𝑚 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑚 ) ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
42 35 41 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝑚 𝐺 𝑚 ) “ ( 𝑚 𝐻 𝑚 ) ) )
43 19 21 42 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑋 } ) ) → ∃ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
44 11 43 exlimddv ⊢ ( 𝜑 → ∃ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( 𝐼 ‘ 𝑋 ) ∈ ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
45 44 eliund ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
46 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
47 46 brrelex1i ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → 𝐹 ∈ V )
48 4 47 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
49 48 48 6 6 3 imasubclem3 ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑋 ) = ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑋 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
50 45 49 eleqtrrd ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝑋 𝐾 𝑋 ) )