Metamath Proof Explorer

Theorem imasubc

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
imasubc.c ⊢ C = Base E
imasubc.j ⊢ J = Hom 𝑓 ⁡ E
Assertion imasubc ⊢ φ → K Fn S × S ∧ S ⊆ C ∧ J ↾ S × S = K

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 imasubc.c ⊢ C = Base E
6 imasubc.j ⊢ J = Hom 𝑓 ⁡ E
7 relfull ⊢ Rel ⁡ D Full E
8 7 brrelex1i ⊢ F D Full E G → F ∈ V
9 4 8 syl ⊢ φ → F ∈ V
10 9 9 3 imasubclem2 ⊢ φ → K Fn S × S
11 eqid ⊢ Base D = Base D
12 fullfunc ⊢ D Full E ⊆ D Func E
13 12 ssbri ⊢ F D Full E G → F D Func E G
14 4 13 syl ⊢ φ → F D Func E G
15 11 5 14 funcf1 ⊢ φ → F : Base D ⟶ C
16 15 fimassd ⊢ φ → F A ⊆ C
17 1 16 eqsstrid ⊢ φ → S ⊆ C
18 simprl ⊢ φ ∧ z ∈ S ∧ w ∈ S → z ∈ S
19 18 1 eleqtrdi ⊢ φ ∧ z ∈ S ∧ w ∈ S → z ∈ F A
20 inisegn0a ⊢ z ∈ F A → F -1 z ≠ ∅
21 19 20 syl ⊢ φ ∧ z ∈ S ∧ w ∈ S → F -1 z ≠ ∅
22 simprr ⊢ φ ∧ z ∈ S ∧ w ∈ S → w ∈ S
23 22 1 eleqtrdi ⊢ φ ∧ z ∈ S ∧ w ∈ S → w ∈ F A
24 inisegn0a ⊢ w ∈ F A → F -1 w ≠ ∅
25 23 24 syl ⊢ φ ∧ z ∈ S ∧ w ∈ S → F -1 w ≠ ∅
26 21 25 jca ⊢ φ ∧ z ∈ S ∧ w ∈ S → F -1 z ≠ ∅ ∧ F -1 w ≠ ∅
27 xpnz ⊢ F -1 z ≠ ∅ ∧ F -1 w ≠ ∅ ↔ F -1 z × F -1 w ≠ ∅
28 26 27 sylib ⊢ φ ∧ z ∈ S ∧ w ∈ S → F -1 z × F -1 w ≠ ∅
29 15 ffnd ⊢ φ → F Fn Base D
30 29 ad2antrr ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F Fn Base D
31 simprl ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m ∈ F -1 z
32 fniniseg ⊢ F Fn Base D → m ∈ F -1 z ↔ m ∈ Base D ∧ F ⁡ m = z
33 32 biimpa ⊢ F Fn Base D ∧ m ∈ F -1 z → m ∈ Base D ∧ F ⁡ m = z
34 30 31 33 syl2anc ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m ∈ Base D ∧ F ⁡ m = z
35 34 simprd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F ⁡ m = z
36 simprr ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → n ∈ F -1 w
37 fniniseg ⊢ F Fn Base D → n ∈ F -1 w ↔ n ∈ Base D ∧ F ⁡ n = w
38 37 biimpa ⊢ F Fn Base D ∧ n ∈ F -1 w → n ∈ Base D ∧ F ⁡ n = w
39 30 36 38 syl2anc ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → n ∈ Base D ∧ F ⁡ n = w
40 39 simprd ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F ⁡ n = w
41 35 40 oveq12d ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F ⁡ m Hom ⁡ E F ⁡ n = z Hom ⁡ E w
42 eqid ⊢ Hom ⁡ E = Hom ⁡ E
43 4 ad2antrr ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → F D Full E G
44 34 simpld ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m ∈ Base D
45 39 simpld ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → n ∈ Base D
46 11 42 2 43 44 45 fullfo ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m G n : m H n ⟶ onto F ⁡ m Hom ⁡ E F ⁡ n
47 foeq3 ⊢ F ⁡ m Hom ⁡ E F ⁡ n = z Hom ⁡ E w → m G n : m H n ⟶ onto F ⁡ m Hom ⁡ E F ⁡ n ↔ m G n : m H n ⟶ onto z Hom ⁡ E w
48 47 biimpa ⊢ F ⁡ m Hom ⁡ E F ⁡ n = z Hom ⁡ E w ∧ m G n : m H n ⟶ onto F ⁡ m Hom ⁡ E F ⁡ n → m G n : m H n ⟶ onto z Hom ⁡ E w
49 41 46 48 syl2anc ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m G n : m H n ⟶ onto z Hom ⁡ E w
50 foima ⊢ m G n : m H n ⟶ onto z Hom ⁡ E w → m G n m H n = z Hom ⁡ E w
51 49 50 syl ⊢ φ ∧ z ∈ S ∧ w ∈ S ∧ m ∈ F -1 z ∧ n ∈ F -1 w → m G n m H n = z Hom ⁡ E w
52 51 ralrimivva ⊢ φ ∧ z ∈ S ∧ w ∈ S → ∀ m ∈ F -1 z ∀ n ∈ F -1 w m G n m H n = z Hom ⁡ E w
53 fveq2 ⊢ p = m n → G ⁡ p = G ⁡ m n
54 df-ov ⊢ m G n = G ⁡ m n
55 53 54 eqtr4di ⊢ p = m n → G ⁡ p = m G n
56 fveq2 ⊢ p = m n → H ⁡ p = H ⁡ m n
57 df-ov ⊢ m H n = H ⁡ m n
58 56 57 eqtr4di ⊢ p = m n → H ⁡ p = m H n
59 55 58 imaeq12d ⊢ p = m n → G ⁡ p H ⁡ p = m G n m H n
60 59 eqeq1d ⊢ p = m n → G ⁡ p H ⁡ p = z Hom ⁡ E w ↔ m G n m H n = z Hom ⁡ E w
61 60 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
62 52 61 sylibr ⊢ φ ∧ z ∈ S ∧ w ∈ S → ∀ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p = z Hom ⁡ E w
63 iuneqconst2 ⊢ F -1 z × F -1 w ≠ ∅ ∧ ∀ 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
64 28 62 63 syl2anc ⊢ φ ∧ z ∈ S ∧ w ∈ S → ⋃ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p = z Hom ⁡ E w
65 9 adantr ⊢ φ ∧ z ∈ S ∧ w ∈ S → F ∈ V
66 65 65 18 22 3 imasubclem3 ⊢ φ ∧ z ∈ S ∧ w ∈ S → z K w = ⋃ p ∈ F -1 z × F -1 w G ⁡ p H ⁡ p
67 17 adantr ⊢ φ ∧ z ∈ S ∧ w ∈ S → S ⊆ C
68 67 18 sseldd ⊢ φ ∧ z ∈ S ∧ w ∈ S → z ∈ C
69 67 22 sseldd ⊢ φ ∧ z ∈ S ∧ w ∈ S → w ∈ C
70 6 5 42 68 69 homfval ⊢ φ ∧ z ∈ S ∧ w ∈ S → z J w = z Hom ⁡ E w
71 64 66 70 3eqtr4rd ⊢ φ ∧ z ∈ S ∧ w ∈ S → z J w = z K w
72 71 ralrimivva ⊢ φ → ∀ z ∈ S ∀ w ∈ S z J w = z K w
73 fveq2 ⊢ q = z w → J ⁡ q = J ⁡ z w
74 df-ov ⊢ z J w = J ⁡ z w
75 73 74 eqtr4di ⊢ q = z w → J ⁡ q = z J w
76 fveq2 ⊢ q = z w → K ⁡ q = K ⁡ z w
77 df-ov ⊢ z K w = K ⁡ z w
78 76 77 eqtr4di ⊢ q = z w → K ⁡ q = z K w
79 75 78 eqeq12d ⊢ q = z w → J ⁡ q = K ⁡ q ↔ z J w = z K w
80 79 ralxp ⊢ ∀ q ∈ S × S J ⁡ q = K ⁡ q ↔ ∀ z ∈ S ∀ w ∈ S z J w = z K w
81 72 80 sylibr ⊢ φ → ∀ q ∈ S × S J ⁡ q = K ⁡ q
82 6 5 homffn ⊢ J Fn C × C
83 82 a1i ⊢ φ → J Fn C × C
84 xpss12 ⊢ S ⊆ C ∧ S ⊆ C → S × S ⊆ C × C
85 17 17 84 syl2anc ⊢ φ → S × S ⊆ C × C
86 fvreseq1 ⊢ J Fn C × C ∧ K Fn S × S ∧ S × S ⊆ C × C → J ↾ S × S = K ↔ ∀ q ∈ S × S J ⁡ q = K ⁡ q
87 83 10 85 86 syl21anc ⊢ φ → J ↾ S × S = K ↔ ∀ q ∈ S × S J ⁡ q = K ⁡ q
88 81 87 mpbird ⊢ φ → J ↾ S × S = K
89 10 17 88 3jca ⊢ φ → K Fn S × S ∧ S ⊆ C ∧ J ↾ S × S = K