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 )