setc1ocofval

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

		Ref	Expression
	Hypothesis	funcsetc1o.1	$⊢ \underset{˙}{1} = SetCat (1_{𝑜})$
	Assertion	setc1ocofval	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} = comp (\underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	$⊢ \underset{˙}{1} = SetCat (1_{𝑜})$
2		df-ot	$⊢ ⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩ = ⟨⟨⟨\emptyset, \emptyset⟩, \emptyset⟩, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩$
3	2	sneqi	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} = \{⟨⟨⟨\emptyset, \emptyset⟩, \emptyset⟩, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\}$
4		opex	$⊢ ⟨\emptyset, \emptyset⟩ \in V$
5		0ex	$⊢ \emptyset \in V$
6		snex	$⊢ \{⟨\emptyset, \emptyset, \emptyset⟩\} \in V$
7		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
8	7	fveq2i	$⊢ SetCat (1_{𝑜}) = SetCat (\{\emptyset\})$
9	1 8	eqtri	$⊢ \underset{˙}{1} = SetCat (\{\emptyset\})$
10		snex	$⊢ \{\emptyset\} \in V$
11	10	a1i	$⊢ ⊤ \to \{\emptyset\} \in V$
12		eqid	$⊢ comp (\underset{˙}{1}) = comp (\underset{˙}{1})$
13	9 11 12	setccofval	$⊢ ⊤ \to comp (\underset{˙}{1}) = (v \in (\{\emptyset\} \times \{\emptyset\}), z \in \{\emptyset\} ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
14	13	mptru	$⊢ comp (\underset{˙}{1}) = (v \in (\{\emptyset\} \times \{\emptyset\}), z \in \{\emptyset\} ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
15	5 5	xpsn	$⊢ \{\emptyset\} \times \{\emptyset\} = \{⟨\emptyset, \emptyset⟩\}$
16		eqid	$⊢ \{\emptyset\} = \{\emptyset\}$
17		eqid	$⊢ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f) = (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f)$
18	15 16 17	mpoeq123i	$⊢ (v \in (\{\emptyset\} \times \{\emptyset\}), z \in \{\emptyset\} ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f)) = (v \in \{⟨\emptyset, \emptyset⟩\}, z \in \{\emptyset\} ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
19	14 18	eqtri	$⊢ comp (\underset{˙}{1}) = (v \in \{⟨\emptyset, \emptyset⟩\}, z \in \{\emptyset\} ⟼ (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f))$
20	5 5	op2ndd	$⊢ v = ⟨\emptyset, \emptyset⟩ \to 2^{nd} (v) = \emptyset$
21	20	oveq2d	$⊢ v = ⟨\emptyset, \emptyset⟩ \to z^{2^{nd} (v)} = z^{\emptyset}$
22	5 5	op1std	$⊢ v = ⟨\emptyset, \emptyset⟩ \to 1^{st} (v) = \emptyset$
23	20 22	oveq12d	$⊢ v = ⟨\emptyset, \emptyset⟩ \to {2^{nd} (v)}^{1^{st} (v)} = \emptyset^{\emptyset}$
24		0map0sn0	$⊢ \emptyset^{\emptyset} = \{\emptyset\}$
25	23 24	eqtrdi	$⊢ v = ⟨\emptyset, \emptyset⟩ \to {2^{nd} (v)}^{1^{st} (v)} = \{\emptyset\}$
26		eqidd	$⊢ v = ⟨\emptyset, \emptyset⟩ \to g \circ f = g \circ f$
27	21 25 26	mpoeq123dv	$⊢ v = ⟨\emptyset, \emptyset⟩ \to (g \in (z^{2^{nd} (v)}), f \in ({2^{nd} (v)}^{1^{st} (v)}) ⟼ g \circ f) = (g \in (z^{\emptyset}), f \in \{\emptyset\} ⟼ g \circ f)$
28		oveq1	$⊢ z = \emptyset \to z^{\emptyset} = \emptyset^{\emptyset}$
29	28 24	eqtrdi	$⊢ z = \emptyset \to z^{\emptyset} = \{\emptyset\}$
30		eqidd	$⊢ z = \emptyset \to \{\emptyset\} = \{\emptyset\}$
31		eqidd	$⊢ z = \emptyset \to g \circ f = g \circ f$
32	29 30 31	mpoeq123dv	$⊢ z = \emptyset \to (g \in (z^{\emptyset}), f \in \{\emptyset\} ⟼ g \circ f) = (g \in \{\emptyset\}, f \in \{\emptyset\} ⟼ g \circ f)$
33		eqid	$⊢ (g \in \{\emptyset\}, f \in \{\emptyset\} ⟼ g \circ f) = (g \in \{\emptyset\}, f \in \{\emptyset\} ⟼ g \circ f)$
34		coeq1	$⊢ g = \emptyset \to g \circ f = \emptyset \circ f$
35		co01	$⊢ \emptyset \circ f = \emptyset$
36	34 35	eqtrdi	$⊢ g = \emptyset \to g \circ f = \emptyset$
37		eqidd	$⊢ f = \emptyset \to \emptyset = \emptyset$
38	33 36 37	mposn	$⊢ (\emptyset \in V \land \emptyset \in V \land \emptyset \in V) \to (g \in \{\emptyset\}, f \in \{\emptyset\} ⟼ g \circ f) = \{⟨⟨\emptyset, \emptyset⟩, \emptyset⟩\}$
39	5 5 5 38	mp3an	$⊢ (g \in \{\emptyset\}, f \in \{\emptyset\} ⟼ g \circ f) = \{⟨⟨\emptyset, \emptyset⟩, \emptyset⟩\}$
40	32 39	eqtrdi	$⊢ z = \emptyset \to (g \in (z^{\emptyset}), f \in \{\emptyset\} ⟼ g \circ f) = \{⟨⟨\emptyset, \emptyset⟩, \emptyset⟩\}$
41		df-ot	$⊢ ⟨\emptyset, \emptyset, \emptyset⟩ = ⟨⟨\emptyset, \emptyset⟩, \emptyset⟩$
42	41	sneqi	$⊢ \{⟨\emptyset, \emptyset, \emptyset⟩\} = \{⟨⟨\emptyset, \emptyset⟩, \emptyset⟩\}$
43	40 42	eqtr4di	$⊢ z = \emptyset \to (g \in (z^{\emptyset}), f \in \{\emptyset\} ⟼ g \circ f) = \{⟨\emptyset, \emptyset, \emptyset⟩\}$
44	19 27 43	mposn	$⊢ (⟨\emptyset, \emptyset⟩ \in V \land \emptyset \in V \land \{⟨\emptyset, \emptyset, \emptyset⟩\} \in V) \to comp (\underset{˙}{1}) = \{⟨⟨⟨\emptyset, \emptyset⟩, \emptyset⟩, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\}$
45	4 5 6 44	mp3an	$⊢ comp (\underset{˙}{1}) = \{⟨⟨⟨\emptyset, \emptyset⟩, \emptyset⟩, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\}$
46	3 45	eqtr4i	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} = comp (\underset{˙}{1})$

Metamath Proof Explorer

Theorem setc1ocofval

Proof