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

Metamath Proof Explorer

Theorem setc1ocofval

Description: Composition in the trivial category. (Contributed by Zhi Wang, 22-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 funcsetc1o.1 ⊢ 1 = ( SetCat ‘ 1o )
2 df-ot ⊢ ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ = ⟨ ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩
3 2 sneqi ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } = { ⟨ ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ }
4 opex ⊢ ⟨ ∅ , ∅ ⟩ ∈ V
5 0ex ⊢ ∅ ∈ V
6 snex ⊢ { ⟨ ∅ , ∅ , ∅ ⟩ } ∈ V
7 df1o2 ⊢ 1o = { ∅ }
8 7 fveq2i ⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ { ∅ } )
9 1 8 eqtri ⊢ 1 = ( SetCat ‘ { ∅ } )
10 snex ⊢ { ∅ } ∈ V
11 10 a1i ⊢ ( ⊤ → { ∅ } ∈ V )
12 eqid ⊢ ( comp ‘ 1 ) = ( comp ‘ 1 )
13 9 11 12 setccofval ⊢ ( ⊤ → ( comp ‘ 1 ) = ( 𝑣 ∈ ( { ∅ } × { ∅ } ) , 𝑧 ∈ { ∅ } ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) )
14 13 mptru ⊢ ( comp ‘ 1 ) = ( 𝑣 ∈ ( { ∅ } × { ∅ } ) , 𝑧 ∈ { ∅ } ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
15 5 5 xpsn ⊢ ( { ∅ } × { ∅ } ) = { ⟨ ∅ , ∅ ⟩ }
16 eqid ⊢ { ∅ } = { ∅ }
17 eqid ⊢ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) )
18 15 16 17 mpoeq123i ⊢ ( 𝑣 ∈ ( { ∅ } × { ∅ } ) , 𝑧 ∈ { ∅ } ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) ) = ( 𝑣 ∈ { ⟨ ∅ , ∅ ⟩ } , 𝑧 ∈ { ∅ } ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
19 14 18 eqtri ⊢ ( comp ‘ 1 ) = ( 𝑣 ∈ { ⟨ ∅ , ∅ ⟩ } , 𝑧 ∈ { ∅ } ↦ ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) )
20 5 5 op2ndd ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( 2nd ‘ 𝑣 ) = ∅ )
21 20 oveq2d ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) = ( 𝑧 ↑m ∅ ) )
22 5 5 op1std ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( 1st ‘ 𝑣 ) = ∅ )
23 20 22 oveq12d ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) = ( ∅ ↑m ∅ ) )
24 0map0sn0 ⊢ ( ∅ ↑m ∅ ) = { ∅ }
25 23 24 eqtrdi ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) = { ∅ } )
26 eqidd ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
27 21 25 26 mpoeq123dv ⊢ ( 𝑣 = ⟨ ∅ , ∅ ⟩ → ( 𝑔 ∈ ( 𝑧 ↑m ( 2nd ‘ 𝑣 ) ) , 𝑓 ∈ ( ( 2nd ‘ 𝑣 ) ↑m ( 1st ‘ 𝑣 ) ) ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ ( 𝑧 ↑m ∅ ) , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) )
28 oveq1 ⊢ ( 𝑧 = ∅ → ( 𝑧 ↑m ∅ ) = ( ∅ ↑m ∅ ) )
29 28 24 eqtrdi ⊢ ( 𝑧 = ∅ → ( 𝑧 ↑m ∅ ) = { ∅ } )
30 eqidd ⊢ ( 𝑧 = ∅ → { ∅ } = { ∅ } )
31 eqidd ⊢ ( 𝑧 = ∅ → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
32 29 30 31 mpoeq123dv ⊢ ( 𝑧 = ∅ → ( 𝑔 ∈ ( 𝑧 ↑m ∅ ) , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ { ∅ } , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) )
33 eqid ⊢ ( 𝑔 ∈ { ∅ } , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) = ( 𝑔 ∈ { ∅ } , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) )
34 coeq1 ⊢ ( 𝑔 = ∅ → ( 𝑔 ∘ 𝑓 ) = ( ∅ ∘ 𝑓 ) )
35 co01 ⊢ ( ∅ ∘ 𝑓 ) = ∅
36 34 35 eqtrdi ⊢ ( 𝑔 = ∅ → ( 𝑔 ∘ 𝑓 ) = ∅ )
37 eqidd ⊢ ( 𝑓 = ∅ → ∅ = ∅ )
38 33 36 37 mposn ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ∧ ∅ ∈ V ) → ( 𝑔 ∈ { ∅ } , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) = { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ } )
39 5 5 5 38 mp3an ⊢ ( 𝑔 ∈ { ∅ } , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) = { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ }
40 32 39 eqtrdi ⊢ ( 𝑧 = ∅ → ( 𝑔 ∈ ( 𝑧 ↑m ∅ ) , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) = { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ } )
41 df-ot ⊢ ⟨ ∅ , ∅ , ∅ ⟩ = ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩
42 41 sneqi ⊢ { ⟨ ∅ , ∅ , ∅ ⟩ } = { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ }
43 40 42 eqtr4di ⊢ ( 𝑧 = ∅ → ( 𝑔 ∈ ( 𝑧 ↑m ∅ ) , 𝑓 ∈ { ∅ } ↦ ( 𝑔 ∘ 𝑓 ) ) = { ⟨ ∅ , ∅ , ∅ ⟩ } )
44 19 27 43 mposn ⊢ ( ( ⟨ ∅ , ∅ ⟩ ∈ V ∧ ∅ ∈ V ∧ { ⟨ ∅ , ∅ , ∅ ⟩ } ∈ V ) → ( comp ‘ 1 ) = { ⟨ ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } )
45 4 5 6 44 mp3an ⊢ ( comp ‘ 1 ) = { ⟨ ⟨ ⟨ ∅ , ∅ ⟩ , ∅ ⟩ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ }
46 3 45 eqtr4i ⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } = ( comp ‘ 1 )