This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indthinc

Description: An indiscrete category in which all hom-sets have exactly one morphism is a thin category. Constructed here is an indiscrete category where all morphisms are (/) . This is a special case of prsthinc , where .<_ = ( B X. B ) . This theorem also implies a functor from the category of sets to the category of small categories. (Contributed by Zhi Wang, 17-Sep-2024) (Proof shortened by Zhi Wang, 19-Sep-2024)

Ref Expression
Hypotheses indthinc.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
indthinc.h ⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
indthinc.o ⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
indthinc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion indthinc ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 indthinc.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 indthinc.h ⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
3 indthinc.o ⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
4 indthinc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( ( 𝐵 × 𝐵 ) × { 1o } ) )
6 5 f1omo ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
7 df-ov ⊢ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
8 7 eleq2i ⊢ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ 𝑓 ∈ ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
9 8 mobii ⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ ( ( ( 𝐵 × 𝐵 ) × { 1o } ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
10 6 9 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
11 biid ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) )
12 id ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵 )
13 12 ancli ⊢ ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
14 1oex ⊢ 1o ∈ V
15 14 ovconst2 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o )
16 0lt1o ⊢ ∅ ∈ 1o
17 eleq2 ⊢ ( ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o → ( ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ ∅ ∈ 1o ) )
18 16 17 mpbiri ⊢ ( ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
19 13 15 18 3syl ⊢ ( 𝑦 ∈ 𝐵 → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
21 16 a1i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ∅ ∈ 1o )
22 0ov ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) = ∅
23 22 oveqi ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ( 𝑔 ∅ 𝑓 )
24 0ov ⊢ ( 𝑔 ∅ 𝑓 ) = ∅
25 23 24 eqtri ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅
26 25 a1i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅ )
27 14 ovconst2 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) = 1o )
28 27 3adant2 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) = 1o )
29 21 26 28 3eltr4d ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) )
30 29 ad2antrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) )
31 1 2 10 3 4 11 20 30 isthincd2 ⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )