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

Metamath Proof Explorer

Theorem isinito3

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 isinito3 ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )

Proof

Step Hyp Ref Expression
1 isinito2.1 ⊢ 1 = ( SetCat ‘ 1o )
2 isinito2.f ⊢ 𝐹 = ( ( 1st ‘ ( 1 Δfunc 𝐶 ) ) ‘ ∅ )
3 relup ⊢ Rel ( 𝐹 ( 𝐶 UP 1 ) ∅ )
4 1 2 isinito2 ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
5 4 biimpi ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
6 releldm ⊢ ( ( Rel ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∧ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) → 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )
7 3 5 6 sylancr ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )
8 releldmb ⊢ ( Rel ( 𝐹 ( 𝐶 UP 1 ) ∅ ) → ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ↔ ∃ 𝑦 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 ) )
9 3 8 ax-mp ⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ↔ ∃ 𝑦 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 )
10 id ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 )
11 10 up1st2nd ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) 𝑦 )
12 1 setc1ohomfval ⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 1 )
13 11 12 uprcl5 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) ) )
14 eqid ⊢ ( 1 Δfunc 𝐶 ) = ( 1 Δfunc 𝐶 )
15 setc1oterm ⊢ ( SetCat ‘ 1o ) ∈ TermCat
16 1 15 eqeltri ⊢ 1 ∈ TermCat
17 16 a1i ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 1 ∈ TermCat )
18 17 termccd ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 1 ∈ Cat )
19 11 uprcl2 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2nd ‘ 𝐹 ) )
20 19 funcrcl2 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐶 ∈ Cat )
21 1 setc1obas ⊢ 1o = ( Base ‘ 1 )
22 11 21 uprcl3 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ∅ ∈ 1o )
23 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
24 11 23 uprcl4 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ∈ ( Base ‘ 𝐶 ) )
25 14 18 20 21 22 2 23 24 diag11 ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) = ∅ )
26 25 oveq2d ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) ) = ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ ) )
27 1oex ⊢ 1o ∈ V
28 27 ovsn2 ⊢ ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ∅ ) = 1o
29 26 28 eqtrdi ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → ( ∅ { ⟨ ∅ , ∅ , 1o ⟩ } ( ( 1st ‘ 𝐹 ) ‘ 𝐼 ) ) = 1o )
30 13 29 eleqtrd ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝑦 ∈ 1o )
31 el1o ⊢ ( 𝑦 ∈ 1o ↔ 𝑦 = ∅ )
32 30 31 sylib ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝑦 = ∅ )
33 10 32 breqtrd ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ )
34 33 4 sylibr ⊢ ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
35 34 exlimiv ⊢ ( ∃ 𝑦 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) 𝑦 → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
36 9 35 sylbi ⊢ ( 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) → 𝐼 ∈ ( InitO ‘ 𝐶 ) )
37 7 36 impbii ⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ dom ( 𝐹 ( 𝐶 UP 1 ) ∅ ) )