Metamath Proof Explorer

Theorem catsubcat

Description: For any category C , C itself is a (full) subcategory of C , see example 4.3(1.b) in Adamek p. 48. (Contributed by AV, 23-Apr-2020)

Ref Expression
Assertion catsubcat ( 𝐶 ∈ Cat → ( Homf ‘ 𝐶 ) ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssidd ⊢ ( 𝐶 ∈ Cat → ( Base ‘ 𝐶 ) ⊆ ( Base ‘ 𝐶 ) )
2 ssidd ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ⊆ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) )
3 2 ralrimivva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ⊆ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) )
4 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 4 5 homffn ⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
7 6 a1i ⊢ ( 𝐶 ∈ Cat → ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
8 fvexd ⊢ ( 𝐶 ∈ Cat → ( Base ‘ 𝐶 ) ∈ V )
9 7 7 8 isssc ⊢ ( 𝐶 ∈ Cat → ( ( Homf ‘ 𝐶 ) ⊆cat ( Homf ‘ 𝐶 ) ↔ ( ( Base ‘ 𝐶 ) ⊆ ( Base ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ⊆ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ) ) )
10 1 3 9 mpbir2and ⊢ ( 𝐶 ∈ Cat → ( Homf ‘ 𝐶 ) ⊆cat ( Homf ‘ 𝐶 ) )
11 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
12 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
13 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
14 simpr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
15 5 11 12 13 14 catidcl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
16 4 5 11 14 14 homfval ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( Homf ‘ 𝐶 ) 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
17 15 16 eleqtrrd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑥 ) )
18 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
19 13 adantr ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
20 19 adantr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
21 14 adantr ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
22 21 adantr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
23 simpl ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
24 23 adantl ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
25 24 adantr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
26 simpr ⊢ ( ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
27 26 adantl ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
28 27 adantr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
29 4 5 11 21 24 homfval ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
30 29 eleq2d ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ↔ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
31 30 biimpcd ⊢ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) → ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
32 31 adantr ⊢ ( ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) → ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
33 32 impcom ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
34 4 5 11 24 27 homfval ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
35 34 eleq2d ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ↔ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
36 35 biimpd ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
37 36 adantld ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) )
38 37 imp ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
39 5 11 18 20 22 25 28 33 38 catcocl ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
40 4 5 11 21 27 homfval ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
41 40 adantr ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑧 ) )
42 39 41 eleqtrrd ⊢ ( ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) )
43 42 ralrimivva ⊢ ( ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑧 ∈ ( Base ‘ 𝐶 ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) )
44 43 ralrimivva ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) )
45 17 44 jca ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) ) )
46 45 ralrimiva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) ) )
47 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
48 4 12 18 47 7 issubc2 ⊢ ( 𝐶 ∈ Cat → ( ( Homf ‘ 𝐶 ) ∈ ( Subcat ‘ 𝐶 ) ↔ ( ( Homf ‘ 𝐶 ) ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑥 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Homf ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( Homf ‘ 𝐶 ) 𝑧 ) ) ) ) )
49 10 46 48 mpbir2and ⊢ ( 𝐶 ∈ Cat → ( Homf ‘ 𝐶 ) ∈ ( Subcat ‘ 𝐶 ) )