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

Metamath Proof Explorer

Theorem setc1ohomfval

Description: Set of morphisms of the trivial category. (Contributed by Zhi Wang, 22-Oct-2025)

Ref Expression
Hypothesis funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
Assertion setc1ohomfval { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 1 )

Proof

Step Hyp Ref Expression
1 funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
2 df-ot ⊢ ⟨ ∅ , ∅ , 1o ⟩ = ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩
3 2 sneqi ⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = { ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩ }
4 0ex ⊢ ∅ ∈ V
5 1oex ⊢ 1o ∈ V
6 df1o2 ⊢ 1o = { ∅ }
7 6 fveq2i ⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ { ∅ } )
8 1 7 eqtri ⊢ 1 = ( SetCat ‘ { ∅ } )
9 p0ex ⊢ { ∅ } ∈ V
10 9 a1i ⊢ ( ⊤ → { ∅ } ∈ V )
11 eqid ⊢ ( Hom ‘ 1 ) = ( Hom ‘ 1 )
12 8 10 11 setchomfval ⊢ ( ⊤ → ( Hom ‘ 1 ) = ( 𝑥 ∈ { ∅ } , 𝑦 ∈ { ∅ } ↦ ( 𝑦 ↑m 𝑥 ) ) )
13 12 mptru ⊢ ( Hom ‘ 1 ) = ( 𝑥 ∈ { ∅ } , 𝑦 ∈ { ∅ } ↦ ( 𝑦 ↑m 𝑥 ) )
14 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝑦 ↑m 𝑥 ) = ( 𝑦 ↑m ∅ ) )
15 oveq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ↑m ∅ ) = ( ∅ ↑m ∅ ) )
16 0map0sn0 ⊢ ( ∅ ↑m ∅ ) = { ∅ }
17 16 6 eqtr4i ⊢ ( ∅ ↑m ∅ ) = 1o
18 15 17 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑦 ↑m ∅ ) = 1o )
19 13 14 18 mposn ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ∧ 1o ∈ V ) → ( Hom ‘ 1 ) = { ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩ } )
20 4 4 5 19 mp3an ⊢ ( Hom ‘ 1 ) = { ⟨ ⟨ ∅ , ∅ ⟩ , 1o ⟩ }
21 3 20 eqtr4i ⊢ { ⟨ ∅ , ∅ , 1o ⟩ } = ( Hom ‘ 1 )