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

Metamath Proof Explorer

Theorem imasubc3

Description: An image of a functor injective on objects is a subcategory. Remark 4.2(3) of Adamek p. 48. (Contributed by Zhi Wang, 7-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2 imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4 imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 imasubc3.f ⊢ ( 𝜑 → Fun ◡ 𝐹 )
6 eqid ⊢ ( Homf ‘ 𝐸 ) = ( Homf ‘ 𝐸 )
7 1 2 3 4 6 imassc ⊢ ( 𝜑 → 𝐾 ⊆cat ( Homf ‘ 𝐸 ) )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
9 eqid ⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
11 1 2 3 8 9 10 imaid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( Id ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) )
12 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
13 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
15 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
16 13 14 4 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
17 df-f1 ⊢ ( 𝐹 : ( Base ‘ 𝐷 ) –1-1→ ( Base ‘ 𝐸 ) ↔ ( 𝐹 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) ∧ Fun ◡ 𝐹 ) )
18 16 5 17 sylanbrc ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐷 ) –1-1→ ( Base ‘ 𝐸 ) )
19 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝐹 : ( Base ‘ 𝐷 ) –1-1→ ( Base ‘ 𝐸 ) )
20 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑎 ∈ 𝑆 )
21 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑏 ∈ 𝑆 )
22 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑐 ∈ 𝑆 )
23 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) )
24 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) )
25 1 2 3 12 13 14 15 19 20 21 22 23 24 imaf1co ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐸 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) )
26 25 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑆 ) ) → ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐸 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) )
27 26 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐸 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) )
28 11 27 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( ( ( Id ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) ∧ ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐸 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) ) )
29 28 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ( ( ( Id ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) ∧ ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐸 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) ) )
30 4 funcrcl3 ⊢ ( 𝜑 → 𝐸 ∈ Cat )
31 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
32 31 brrelex1i ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → 𝐹 ∈ V )
33 4 32 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
34 33 33 3 imasubclem2 ⊢ ( 𝜑 → 𝐾 Fn ( 𝑆 × 𝑆 ) )
35 6 9 15 30 34 issubc2 ⊢ ( 𝜑 → ( 𝐾 ∈ ( Subcat ‘ 𝐸 ) ↔ ( 𝐾 ⊆cat ( Homf ‘ 𝐸 ) ∧ ∀ 𝑎 ∈ 𝑆 ( ( ( Id ‘ 𝐸 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) ∧ ∀ 𝑏 ∈ 𝑆 ∀ 𝑐 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐸 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) ) ) ) )
36 7 29 35 mpbir2and ⊢ ( 𝜑 → 𝐾 ∈ ( Subcat ‘ 𝐸 ) )