Theorem imasubc2

Description: An image of a full functor is a (full) 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	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
	imasubc.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 )
Assertion	imasubc2	⊢ ( 𝜑 → 𝐾 ∈ ( Subcat ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		imasubc.s	⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2		imasubc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
3		imasubc.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4		imasubc.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 )
5		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
6		eqid	⊢ ( Homf ‘ 𝐸 ) = ( Homf ‘ 𝐸 )
7	1 2 3 4 5 6	imasubc	⊢ ( 𝜑 → ( 𝐾 Fn ( 𝑆 × 𝑆 ) ∧ 𝑆 ⊆ ( Base ‘ 𝐸 ) ∧ ( ( Homf ‘ 𝐸 ) ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 ) )
8	7	simp3d	⊢ ( 𝜑 → ( ( Homf ‘ 𝐸 ) ↾ ( 𝑆 × 𝑆 ) ) = 𝐾 )
9		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
10	9	ssbri	⊢ ( 𝐹 ( 𝐷 Full 𝐸 ) 𝐺 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
11	4 10	syl	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
12	11	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
13	7	simp2d	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐸 ) )
14	5 6 12 13	fullsubc	⊢ ( 𝜑 → ( ( Homf ‘ 𝐸 ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( Subcat ‘ 𝐸 ) )
15	8 14	eqeltrrd	⊢ ( 𝜑 → 𝐾 ∈ ( Subcat ‘ 𝐸 ) )