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

Metamath Proof Explorer

Theorem setc1oid

Description: The identity morphism of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025)

Ref Expression
Hypotheses funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
setc1oid.i ⊢ 𝐼 = ( Id ‘ 1 )
Assertion setc1oid ( 𝐼 ‘ ∅ ) = ∅

Proof

Step Hyp Ref Expression
1 funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
2 setc1oid.i ⊢ 𝐼 = ( Id ‘ 1 )
3 1oex ⊢ 1o ∈ V
4 3 a1i ⊢ ( ⊤ → 1o ∈ V )
5 0lt1o ⊢ ∅ ∈ 1o
6 5 a1i ⊢ ( ⊤ → ∅ ∈ 1o )
7 1 2 4 6 setcid ⊢ ( ⊤ → ( 𝐼 ‘ ∅ ) = ( I ↾ ∅ ) )
8 7 mptru ⊢ ( 𝐼 ‘ ∅ ) = ( I ↾ ∅ )
9 res0 ⊢ ( I ↾ ∅ ) = ∅
10 8 9 eqtri ⊢ ( 𝐼 ‘ ∅ ) = ∅