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

Metamath Proof Explorer

Theorem isinito4

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 ) )
isinito4.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )
Assertion isinito4 ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 isinito4.1 ⊢ ( 𝜑 → 1 ∈ TermCat )
2 isinito4.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 1 ) )
3 isinito4.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )
4 eqid ⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ 1o )
5 eqid ⊢ ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) = ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ )
6 4 5 isinito3 ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ( 𝐶 UP ( SetCat ‘ 1o ) ) ∅ ) )
7 4 setc1obas ⊢ 1o = ( Base ‘ ( SetCat ‘ 1o ) )
8 eqid ⊢ ( Base ‘ 1 ) = ( Base ‘ 1 )
9 0lt1o ⊢ ∅ ∈ 1o
10 9 a1i ⊢ ( 𝜑 → ∅ ∈ 1o )
11 3 func1st2nd ⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2nd ‘ 𝐹 ) )
12 11 funcrcl2 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
13 4 5 12 funcsetc1ocl ⊢ ( 𝜑 → ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ∈ ( 𝐶 Func ( SetCat ‘ 1o ) ) )
14 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
15 14 a1i ⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ TermCat )
16 7 8 10 2 13 3 15 1 uobeqterm ⊢ ( 𝜑 → dom ( ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ( 𝐶 UP ( SetCat ‘ 1o ) ) ∅ ) = dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) )
17 16 eleq2d ⊢ ( 𝜑 → ( 𝐼 ∈ dom ( ( ( 1st ‘ ( ( SetCat ‘ 1o ) Δfunc 𝐶 ) ) ‘ ∅ ) ( 𝐶 UP ( SetCat ‘ 1o ) ) ∅ ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )
18 6 17 bitrid ⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) 𝑋 ) ) )