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 ⊢ S = F A
imasubc.h ⊢ H = Hom ⁡ D
imasubc.k ⊢ K = x ∈ S , y ∈ S ⟼ ⋃ p ∈ F -1 x × F -1 y G ⁡ p H ⁡ p
imasubc.f ⊢ φ → F D Full E G
Assertion imasubc2 ⊢ φ → K ∈ Subcat ⁡ E

Proof

Step Hyp Ref Expression
1 imasubc.s ⊢ S = F A
2 imasubc.h ⊢ H = Hom ⁡ D
3 imasubc.k ⊢ K = x ∈ S , y ∈ S ⟼ ⋃ p ∈ F -1 x × F -1 y G ⁡ p H ⁡ p
4 imasubc.f ⊢ φ → F D Full E G
5 eqid ⊢ Base E = Base E
6 eqid ⊢ Hom 𝑓 ⁡ E = Hom 𝑓 ⁡ E
7 1 2 3 4 5 6 imasubc ⊢ φ → K Fn S × S ∧ S ⊆ Base E ∧ Hom 𝑓 ⁡ E ↾ S × S = K
8 7 simp3d ⊢ φ → Hom 𝑓 ⁡ E ↾ S × S = K
9 fullfunc ⊢ D Full E ⊆ D Func E
10 9 ssbri ⊢ F D Full E G → F D Func E G
11 4 10 syl ⊢ φ → F D Func E G
12 11 funcrcl3 ⊢ φ → E ∈ Cat
13 7 simp2d ⊢ φ → S ⊆ Base E
14 5 6 12 13 fullsubc ⊢ φ → Hom 𝑓 ⁡ E ↾ S × S ∈ Subcat ⁡ E
15 8 14 eqeltrrd ⊢ φ → K ∈ Subcat ⁡ E