Metamath Proof Explorer

Theorem subthinc

Description: A subcategory of a thin category is thin. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypotheses subthinc.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
subthinc.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
subthinc.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
Assertion subthinc ( 𝜑 → 𝐷 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 subthinc.1 ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
2 subthinc.j ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
3 subthinc.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqidd ⊢ ( 𝜑 → dom dom 𝐽 = dom dom 𝐽 )
6 2 5 subcfn ⊢ ( 𝜑 → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
7 2 6 4 subcss1 ⊢ ( 𝜑 → dom dom 𝐽 ⊆ ( Base ‘ 𝐶 ) )
8 1 4 3 6 7 rescbas ⊢ ( 𝜑 → dom dom 𝐽 = ( Base ‘ 𝐷 ) )
9 1 4 3 6 7 reschom ⊢ ( 𝜑 → 𝐽 = ( Hom ‘ 𝐷 ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
11 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
12 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝑥 ∈ dom dom 𝐽 )
14 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝑦 ∈ dom dom 𝐽 )
15 10 11 12 13 14 subcss2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → ( 𝑥 𝐽 𝑦 ) ⊆ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
16 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝐶 ∈ ThinCat )
17 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → dom dom 𝐽 ⊆ ( Base ‘ 𝐶 ) )
18 17 13 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
19 17 14 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
20 16 18 19 4 12 thincmo ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
21 mosssn2 ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ∃ 𝑓 ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⊆ { 𝑓 } )
22 20 21 sylib ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → ∃ 𝑓 ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⊆ { 𝑓 } )
23 sstr2 ⊢ ( ( 𝑥 𝐽 𝑦 ) ⊆ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⊆ { 𝑓 } → ( 𝑥 𝐽 𝑦 ) ⊆ { 𝑓 } ) )
24 23 eximdv ⊢ ( ( 𝑥 𝐽 𝑦 ) ⊆ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) → ( ∃ 𝑓 ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⊆ { 𝑓 } → ∃ 𝑓 ( 𝑥 𝐽 𝑦 ) ⊆ { 𝑓 } ) )
25 15 22 24 sylc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → ∃ 𝑓 ( 𝑥 𝐽 𝑦 ) ⊆ { 𝑓 } )
26 mosssn2 ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ↔ ∃ 𝑓 ( 𝑥 𝐽 𝑦 ) ⊆ { 𝑓 } )
27 25 26 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom dom 𝐽 ∧ 𝑦 ∈ dom dom 𝐽 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) )
28 1 2 subccat ⊢ ( 𝜑 → 𝐷 ∈ Cat )
29 8 9 27 28 isthincd ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )