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 ‘ 𝐸 ) )