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

Metamath Proof Explorer

Theorem isinito4a

Description: The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 17-Nov-2025)

Ref Expression
Hypotheses isinito4.1 ⊢ ( 𝜑 → 1 ∈ TermCat )
isinito4.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 1 ) )
isinito4a.f ⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ 𝑋 )
Assertion isinito4a ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 isinito4.1 ⊢ ( 𝜑 → 1 ∈ TermCat )
2 isinito4.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 1 ) )
3 isinito4a.f ⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ 𝑋 )
4 initorcl ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )
5 4 anim2i ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝜑 ∧ 𝐶 ∈ Cat ) )
6 uobrcl ⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) → ( 𝐶 ∈ Cat ∧ 1 ∈ Cat ) )
7 6 simpld ⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) → 𝐶 ∈ Cat )
8 7 anim2i ⊢ ( ( 𝜑 ∧ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) → ( 𝜑 ∧ 𝐶 ∈ Cat ) )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 1 ∈ TermCat )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝑋 ∈ ( Base ‘ 1 ) )
11 eqid ⊢ ( 1 Δfunc 𝐶 ) = ( 1 Δfunc 𝐶 )
12 9 termccd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 1 ∈ Cat )
13 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
14 eqid ⊢ ( Base ‘ 1 ) = ( Base ‘ 1 )
15 11 12 13 14 10 3 diag1cl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → 𝐹 ∈ ( 𝐶 Func 1 ) )
16 9 10 15 isinito4 ⊢ ( ( 𝜑 ∧ 𝐶 ∈ Cat ) → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )
17 5 8 16 pm5.21nd ⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )