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

Metamath Proof Explorer

Theorem initc

Description: Sets with empty base are the only initial objects in the category of small categories. Example 7.2(3) of Adamek p. 101. (Contributed by Zhi Wang, 15-Nov-2025)

Ref Expression
Assertion initc ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ↔ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑑 ∈ Cat ) → 𝐶 ∈ V )
2 simplr ⊢ ( ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑑 ∈ Cat ) → ∅ = ( Base ‘ 𝐶 ) )
3 simpr ⊢ ( ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑑 ∈ Cat ) → 𝑑 ∈ Cat )
4 1 2 3 0funcg ⊢ ( ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑑 ∈ Cat ) → ( 𝐶 Func 𝑑 ) = { ⟨ ∅ , ∅ ⟩ } )
5 opex ⊢ ⟨ ∅ , ∅ ⟩ ∈ V
6 sneq ⊢ ( 𝑓 = ⟨ ∅ , ∅ ⟩ → { 𝑓 } = { ⟨ ∅ , ∅ ⟩ } )
7 6 eqeq2d ⊢ ( 𝑓 = ⟨ ∅ , ∅ ⟩ → ( ( 𝐶 Func 𝑑 ) = { 𝑓 } ↔ ( 𝐶 Func 𝑑 ) = { ⟨ ∅ , ∅ ⟩ } ) )
8 5 7 spcev ⊢ ( ( 𝐶 Func 𝑑 ) = { ⟨ ∅ , ∅ ⟩ } → ∃ 𝑓 ( 𝐶 Func 𝑑 ) = { 𝑓 } )
9 4 8 syl ⊢ ( ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑑 ∈ Cat ) → ∃ 𝑓 ( 𝐶 Func 𝑑 ) = { 𝑓 } )
10 eusn ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) ↔ ∃ 𝑓 ( 𝐶 Func 𝑑 ) = { 𝑓 } )
11 9 10 sylibr ⊢ ( ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ∧ 𝑑 ∈ Cat ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) )
12 11 ralrimiva ⊢ ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) → ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) )
13 0cat ⊢ ∅ ∈ Cat
14 oveq2 ⊢ ( 𝑑 = ∅ → ( 𝐶 Func 𝑑 ) = ( 𝐶 Func ∅ ) )
15 14 eleq2d ⊢ ( 𝑑 = ∅ → ( 𝑓 ∈ ( 𝐶 Func 𝑑 ) ↔ 𝑓 ∈ ( 𝐶 Func ∅ ) ) )
16 15 eubidv ⊢ ( 𝑑 = ∅ → ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝐶 Func ∅ ) ) )
17 16 rspcv ⊢ ( ∅ ∈ Cat → ( ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func ∅ ) ) )
18 13 17 ax-mp ⊢ ( ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func ∅ ) )
19 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func ∅ ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func ∅ ) )
20 funcrcl ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → ( 𝐶 ∈ Cat ∧ ∅ ∈ Cat ) )
21 20 simpld ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → 𝐶 ∈ Cat )
22 21 elexd ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → 𝐶 ∈ V )
23 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
24 base0 ⊢ ∅ = ( Base ‘ ∅ )
25 eqidd ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → ∅ = ∅ )
26 id ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → 𝑓 ∈ ( 𝐶 Func ∅ ) )
27 23 24 25 26 func0g2 ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → ( Base ‘ 𝐶 ) = ∅ )
28 27 eqcomd ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → ∅ = ( Base ‘ 𝐶 ) )
29 22 28 jca ⊢ ( 𝑓 ∈ ( 𝐶 Func ∅ ) → ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) )
30 29 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐶 Func ∅ ) → ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) )
31 18 19 30 3syl ⊢ ( ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) → ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) )
32 12 31 impbii ⊢ ( ( 𝐶 ∈ V ∧ ∅ = ( Base ‘ 𝐶 ) ) ↔ ∀ 𝑑 ∈ Cat ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝑑 ) )