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

Metamath Proof Explorer

Theorem isinito2

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

Ref Expression
Hypotheses isinito2.1 ⊢ 1 = ( SetCat ‘ 1o )
isinito2.f ⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
Assertion isinito2 ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )

Proof

Step Hyp Ref Expression
1 isinito2.1 ⊢ 1 = ( SetCat ‘ 1o )
2 isinito2.f ⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
3 initorcl ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 4 initoo2 ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ∈ ( Base ‘ 𝐶 ) )
6 1 2 3 5 isinito2lem ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) )
7 6 ibi ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
8 id ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
9 8 up1st2nd ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) ∅ )
10 9 uprcl2 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → ( 1st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2nd ‘ 𝐹 ) )
11 10 funcrcl2 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐶 ∈ Cat )
12 9 4 uprcl4 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ∈ ( Base ‘ 𝐶 ) )
13 1 2 11 12 isinito2lem ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) )
14 13 ibir ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
15 7 14 impbii ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )