Metamath Proof Explorer

Theorem imassc

Description: An image of a functor satisfies the subcategory subset relation. (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
imassc.f ⊢ φ → F D Func E G
imassc.j ⊢ J = Hom 𝑓 ⁡ E
Assertion imassc ⊢ φ → K ⊆ cat J

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 imassc.f ⊢ φ → F D Func E G
5 imassc.j ⊢ J = Hom 𝑓 ⁡ E
6 eqid ⊢ Base D = Base D
7 eqid ⊢ Base E = Base E
8 6 7 4 funcf1 ⊢ φ → F : Base D ⟶ Base E
9 8 fimassd ⊢ φ → F A ⊆ Base E
10 1 9 eqsstrid ⊢ φ → S ⊆ Base E
11 eqid ⊢ Hom ⁡ E = Hom ⁡ E
12 4 ad2antrr ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F D Func E G
13 6 7 12 funcf1 ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F : Base D ⟶ Base E
14 13 ffnd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F Fn Base D
15 simprl ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m ∈ F -1 z
16 fniniseg ⊢ F Fn Base D → m ∈ F -1 z ↔ m ∈ Base D ∧ F ⁡ m = z
17 16 biimpa ⊢ F Fn Base D ∧ m ∈ F -1 z → m ∈ Base D ∧ F ⁡ m = z
18 14 15 17 syl2anc ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m ∈ Base D ∧ F ⁡ m = z
19 18 simpld ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m ∈ Base D
20 simprr ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → n ∈ F -1 w
21 fniniseg ⊢ F Fn Base D → n ∈ F -1 w ↔ n ∈ Base D ∧ F ⁡ n = w
22 21 biimpa ⊢ F Fn Base D ∧ n ∈ F -1 w → n ∈ Base D ∧ F ⁡ n = w
23 14 20 22 syl2anc ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → n ∈ Base D ∧ F ⁡ n = w
24 23 simpld ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → n ∈ Base D
25 6 2 11 12 19 24 funcf2 ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m G n : m H n ⟶ F ⁡ m Hom ⁡ E F ⁡ n
26 25 fimassd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m G n m H n ⊆ F ⁡ m Hom ⁡ E F ⁡ n
27 18 simprd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F ⁡ m = z
28 23 simprd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F ⁡ n = w
29 27 28 oveq12d ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F ⁡ m Hom ⁡ E F ⁡ n = z Hom ⁡ E w
30 26 29 sseqtrd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m G n m H n ⊆ z Hom ⁡ E w
31 30 ralrimivva ⊢ φ ∧ z ∈ S ∧ w ∈ S → ∀ m ∈ F -1 z ∀ n ∈ F -1 w m G n m H n ⊆ z Hom ⁡ E w
32 iunss ⊢ ⋃ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p ⊆ z Hom ⁡ E w ↔ ∀ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p ⊆ z Hom ⁡ E w
33 fveq2 ⊢ p = m n → G ⁡ p = G ⁡ m n
34 df-ov ⊢ m G n = G ⁡ m n
35 33 34 eqtr4di ⊢ p = m n → G ⁡ p = m G n
36 fveq2 ⊢ p = m n → H ⁡ p = H ⁡ m n
37 df-ov ⊢ m H n = H ⁡ m n
38 36 37 eqtr4di ⊢ p = m n → H ⁡ p = m H n
39 35 38 imaeq12d ⊢ p = m n → G ⁡ p H ⁡ p = m G n m H n
40 39 sseq1d ⊢ p = m n → G ⁡ p H ⁡ p ⊆ z Hom ⁡ E w ↔ m G n m H n ⊆ z Hom ⁡ E w
41 40 ralxp ⊢ ∀ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p ⊆ z Hom ⁡ E w ↔ ∀ m ∈ F -1 z ∀ n ∈ F -1 w m G n m H n ⊆ z Hom ⁡ E w
42 32 41 bitri ⊢ ⋃ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p ⊆ z Hom ⁡ E w ↔ ∀ m ∈ F -1 z ∀ n ∈ F -1 w m G n m H n ⊆ z Hom ⁡ E w
43 31 42 sylibr ⊢ φ ∧ z ∈ S ∧ w ∈ S → ⋃ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p ⊆ z Hom ⁡ E w
44 relfunc ⊢ Rel ⁡ D Func E
45 44 brrelex1i ⊢ F D Func E G → F ∈ V
46 4 45 syl ⊢ φ → F ∈ V
47 46 adantr ⊢ φ ∧ z ∈ S ∧ w ∈ S → F ∈ V
48 simprl ⊢ φ ∧ z ∈ S ∧ w ∈ S → z ∈ S
49 simprr ⊢ φ ∧ z ∈ S ∧ w ∈ S → w ∈ S
50 47 47 48 49 3 imasubclem3 ⊢ φ ∧ z ∈ S ∧ w ∈ S → z K w = ⋃ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p
51 10 adantr ⊢ φ ∧ z ∈ S ∧ w ∈ S → S ⊆ Base E
52 51 48 sseldd ⊢ φ ∧ z ∈ S ∧ w ∈ S → z ∈ Base E
53 51 49 sseldd ⊢ φ ∧ z ∈ S ∧ w ∈ S → w ∈ Base E
54 5 7 11 52 53 homfval ⊢ φ ∧ z ∈ S ∧ w ∈ S → z J w = z Hom ⁡ E w
55 43 50 54 3sstr4d ⊢ φ ∧ z ∈ S ∧ w ∈ S → z K w ⊆ z J w
56 55 ralrimivva ⊢ φ → ∀ z ∈ S ∀ w ∈ S z K w ⊆ z J w
57 46 46 3 imasubclem2 ⊢ φ → K Fn S × S
58 5 7 homffn ⊢ J Fn Base E × Base E
59 58 a1i ⊢ φ → J Fn Base E × Base E
60 fvexd ⊢ φ → Base E ∈ V
61 57 59 60 isssc ⊢ φ → K ⊆ cat J ↔ S ⊆ Base E ∧ ∀ z ∈ S ∀ w ∈ S z K w ⊆ z J w
62 10 56 61 mpbir2and ⊢ φ → K ⊆ cat J