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

Metamath Proof Explorer

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