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 ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
imassc.j ⊢ 𝐽 = ( Homf ‘ 𝐸 )
Assertion imassc ( 𝜑 → 𝐾 ⊆cat 𝐽 )

Proof

Step Hyp Ref Expression
1 imasubc.s ⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2 imasubc.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
3 imasubc.k ⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
4 imassc.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 imassc.j ⊢ 𝐽 = ( Homf ‘ 𝐸 )
6 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8 6 7 4 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
9 8 fimassd ⊢ ( 𝜑 → ( 𝐹 “ 𝐴 ) ⊆ ( Base ‘ 𝐸 ) )
10 1 9 eqsstrid ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐸 ) )
11 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
12 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
13 6 7 12 funcf1 ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝐹 : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
14 13 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝐹 Fn ( Base ‘ 𝐷 ) )
15 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) )
16 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐷 ) → ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ↔ ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑧 ) ) )
17 16 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐷 ) ∧ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ) → ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑧 ) )
18 14 15 17 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑚 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑚 ) = 𝑧 ) )
19 18 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑚 ∈ ( Base ‘ 𝐷 ) )
20 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
21 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐷 ) → ( 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( 𝑛 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑤 ) ) )
22 21 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐷 ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝑛 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑤 ) )
23 14 20 22 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑛 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑤 ) )
24 23 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → 𝑛 ∈ ( Base ‘ 𝐷 ) )
25 6 2 11 12 19 24 funcf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) )
26 25 fimassd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) ⊆ ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) )
27 18 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝐹 ‘ 𝑚 ) = 𝑧 )
28 23 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝐹 ‘ 𝑛 ) = 𝑤 )
29 27 28 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( ( 𝐹 ‘ 𝑚 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
30 26 29 sseqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
31 30 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ∀ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∀ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
32 iunss ⊢ ( ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ↔ ∀ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
33 fveq2 ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑛 ⟩ ) )
34 df-ov ⊢ ( 𝑚 𝐺 𝑛 ) = ( 𝐺 ‘ ⟨ 𝑚 , 𝑛 ⟩ )
35 33 34 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝑚 𝐺 𝑛 ) )
36 fveq2 ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑛 ⟩ ) )
37 df-ov ⊢ ( 𝑚 𝐻 𝑛 ) = ( 𝐻 ‘ ⟨ 𝑚 , 𝑛 ⟩ )
38 36 37 eqtr4di ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝑚 𝐻 𝑛 ) )
39 35 38 imaeq12d ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) )
40 39 sseq1d ⊢ ( 𝑝 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ↔ ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ) )
41 40 ralxp ⊢ ( ∀ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ↔ ∀ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∀ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
42 32 41 bitri ⊢ ( ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) ↔ ∀ 𝑚 ∈ ( ◡ 𝐹 “ { 𝑧 } ) ∀ 𝑛 ∈ ( ◡ 𝐹 “ { 𝑤 } ) ( ( 𝑚 𝐺 𝑛 ) “ ( 𝑚 𝐻 𝑛 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
43 31 42 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) ⊆ ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
44 relfunc ⊢ Rel ( 𝐷 Func 𝐸 )
45 44 brrelex1i ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → 𝐹 ∈ V )
46 4 45 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝐹 ∈ V )
48 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
49 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ 𝑆 )
50 47 47 48 49 3 imasubclem3 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐾 𝑤 ) = ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑧 } ) × ( ◡ 𝐹 “ { 𝑤 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
51 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐸 ) )
52 51 48 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑧 ∈ ( Base ‘ 𝐸 ) )
53 51 49 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → 𝑤 ∈ ( Base ‘ 𝐸 ) )
54 5 7 11 52 53 homfval ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐽 𝑤 ) = ( 𝑧 ( Hom ‘ 𝐸 ) 𝑤 ) )
55 43 50 54 3sstr4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑧 𝐾 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
56 55 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( 𝑧 𝐾 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
57 46 46 3 imasubclem2 ⊢ ( 𝜑 → 𝐾 Fn ( 𝑆 × 𝑆 ) )
58 5 7 homffn ⊢ 𝐽 Fn ( ( Base ‘ 𝐸 ) × ( Base ‘ 𝐸 ) )
59 58 a1i ⊢ ( 𝜑 → 𝐽 Fn ( ( Base ‘ 𝐸 ) × ( Base ‘ 𝐸 ) ) )
60 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) ∈ V )
61 57 59 60 isssc ⊢ ( 𝜑 → ( 𝐾 ⊆cat 𝐽 ↔ ( 𝑆 ⊆ ( Base ‘ 𝐸 ) ∧ ∀ 𝑧 ∈ 𝑆 ∀ 𝑤 ∈ 𝑆 ( 𝑧 𝐾 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) ) ) )
62 10 56 61 mpbir2and ⊢ ( 𝜑 → 𝐾 ⊆cat 𝐽 )