Theorem par2hom

Description: The four hom-sets of the explicit two-object parallel-arrow category. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypothesis	par2hom.h	$$⊢H=\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)$$
Assertion	par2hom	$$⊢\left(\varnothing H\varnothing =\left\{2_{𝑜}\right\}\wedge 1_{𝑜}H{1}_{𝑜}=\left\{2_{𝑜}\right\}\wedge \left(\varnothing H{1}_{𝑜}=2_{𝑜}\wedge 1_{𝑜}H\varnothing =\varnothing \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		par2hom.h	$$⊢H=\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
4		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
5	3 4	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
6		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
7	1 6	parhomval	$$⊢\left(\varnothing \in 2_{𝑜}\wedge \varnothing \in 2_{𝑜}\right)\to \varnothing H\varnothing =if\left(\varnothing =\varnothing ,\left\{2_{𝑜}\right\},if\left(\left(\varnothing =\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
8	5 5 7	mp2an	$$⊢\varnothing H\varnothing =if\left(\varnothing =\varnothing ,\left\{2_{𝑜}\right\},if\left(\left(\varnothing =\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
9		eqid	$$⊢\varnothing =\varnothing$$
10	9	iftruei	$$⊢if\left(\varnothing =\varnothing ,\left\{2_{𝑜}\right\},if\left(\left(\varnothing =\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)=\left\{2_{𝑜}\right\}$$
11	8 10	eqtri	$$⊢\varnothing H\varnothing =\left\{2_{𝑜}\right\}$$
12		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
13	12 4	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
14	1 6	parhomval	$$⊢\left(1_{𝑜}\in 2_{𝑜}\wedge 1_{𝑜}\in 2_{𝑜}\right)\to 1_{𝑜}H{1}_{𝑜}=if\left(1_{𝑜}=1_{𝑜},\left\{2_{𝑜}\right\},if\left(\left(1_{𝑜}=\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
15	13 13 14	mp2an	$$⊢1_{𝑜}H{1}_{𝑜}=if\left(1_{𝑜}=1_{𝑜},\left\{2_{𝑜}\right\},if\left(\left(1_{𝑜}=\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
16		eqid	$$⊢1_{𝑜}=1_{𝑜}$$
17	16	iftruei	$$⊢if\left(1_{𝑜}=1_{𝑜},\left\{2_{𝑜}\right\},if\left(\left(1_{𝑜}=\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)=\left\{2_{𝑜}\right\}$$
18	15 17	eqtri	$$⊢1_{𝑜}H{1}_{𝑜}=\left\{2_{𝑜}\right\}$$
19	1 6	parhomval	$$⊢\left(\varnothing \in 2_{𝑜}\wedge 1_{𝑜}\in 2_{𝑜}\right)\to \varnothing H{1}_{𝑜}=if\left(\varnothing =1_{𝑜},\left\{2_{𝑜}\right\},if\left(\left(\varnothing =\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
20	5 13 19	mp2an	$$⊢\varnothing H{1}_{𝑜}=if\left(\varnothing =1_{𝑜},\left\{2_{𝑜}\right\},if\left(\left(\varnothing =\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
21		1n0	$$⊢1_{𝑜}\ne \varnothing$$
22	21	nesymi	$$⊢\neg \varnothing =1_{𝑜}$$
23	22	iffalsei	$$⊢if\left(\varnothing =1_{𝑜},\left\{2_{𝑜}\right\},if\left(\left(\varnothing =\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)=if\left(\left(\varnothing =\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)$$
24	9 16	pm3.2i	$$⊢\left(\varnothing =\varnothing \wedge 1_{𝑜}=1_{𝑜}\right)$$
25	24	iftruei	$$⊢if\left(\left(\varnothing =\varnothing \wedge 1_{𝑜}=1_{𝑜}\right),2_{𝑜},\varnothing \right)=2_{𝑜}$$
26	20 23 25	3eqtri	$$⊢\varnothing H{1}_{𝑜}=2_{𝑜}$$
27	1 6	parhomval	$$⊢\left(1_{𝑜}\in 2_{𝑜}\wedge \varnothing \in 2_{𝑜}\right)\to 1_{𝑜}H\varnothing =if\left(1_{𝑜}=\varnothing ,\left\{2_{𝑜}\right\},if\left(\left(1_{𝑜}=\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
28	13 5 27	mp2an	$$⊢1_{𝑜}H\varnothing =if\left(1_{𝑜}=\varnothing ,\left\{2_{𝑜}\right\},if\left(\left(1_{𝑜}=\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)$$
29	21	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
30	29	iffalsei	$$⊢if\left(1_{𝑜}=\varnothing ,\left\{2_{𝑜}\right\},if\left(\left(1_{𝑜}=\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)=if\left(\left(1_{𝑜}=\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)$$
31	29	intnanr	$$⊢\neg \left(1_{𝑜}=\varnothing \wedge \varnothing =1_{𝑜}\right)$$
32	31	iffalsei	$$⊢if\left(\left(1_{𝑜}=\varnothing \wedge \varnothing =1_{𝑜}\right),2_{𝑜},\varnothing \right)=\varnothing$$
33	28 30 32	3eqtri	$$⊢1_{𝑜}H\varnothing =\varnothing$$
34	26 33	pm3.2i	$$⊢\left(\varnothing H{1}_{𝑜}=2_{𝑜}\wedge 1_{𝑜}H\varnothing =\varnothing \right)$$
35	11 18 34	3pm3.2i	$$⊢\left(\varnothing H\varnothing =\left\{2_{𝑜}\right\}\wedge 1_{𝑜}H{1}_{𝑜}=\left\{2_{𝑜}\right\}\wedge \left(\varnothing H{1}_{𝑜}=2_{𝑜}\wedge 1_{𝑜}H\varnothing =\varnothing \right)\right)$$