Theorem parswapprop

Description: The concrete transposition fixes the identity, preserves the parallel arrows, and sends the empty-set arrow to the ordinal-one arrow. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypothesis	parswapval.a	$$⊢A=\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)$$
Assertion	parswapprop	$$⊢\left(A\left(2_{𝑜}\right)=2_{𝑜}\wedge \forall t\in 2_{𝑜}A\left(t\right)\in 2_{𝑜}\wedge A\left(\varnothing \right)=1_{𝑜}\right)$$

Proof

Step	Hyp	Ref	Expression
1		parswapval.a	$$⊢A=\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)$$
2		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
3	2	sucid	$$⊢2_{𝑜}\in \mathrm{suc}{2}_{𝑜}$$
4		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
5	3 4	eleqtrri	$$⊢2_{𝑜}\in 3_{𝑜}$$
6	1	parswapval	$$⊢2_{𝑜}\in 3_{𝑜}\to A\left(2_{𝑜}\right)=if\left(2_{𝑜}=2_{𝑜},2_{𝑜},if\left(2_{𝑜}=\varnothing ,1_{𝑜},\varnothing \right)\right)$$
7	5 6	ax-mp	$$⊢A\left(2_{𝑜}\right)=if\left(2_{𝑜}=2_{𝑜},2_{𝑜},if\left(2_{𝑜}=\varnothing ,1_{𝑜},\varnothing \right)\right)$$
8		eqid	$$⊢2_{𝑜}=2_{𝑜}$$
9	8	iftruei	$$⊢if\left(2_{𝑜}=2_{𝑜},2_{𝑜},if\left(2_{𝑜}=\varnothing ,1_{𝑜},\varnothing \right)\right)=2_{𝑜}$$
10	7 9	eqtri	$$⊢A\left(2_{𝑜}\right)=2_{𝑜}$$
11		elelsuc	$$⊢t\in 2_{𝑜}\to t\in \mathrm{suc}{2}_{𝑜}$$
12	11 4	eleqtrrdi	$$⊢t\in 2_{𝑜}\to t\in 3_{𝑜}$$
13	1	parswapval	$$⊢t\in 3_{𝑜}\to A\left(t\right)=if\left(t=2_{𝑜},2_{𝑜},if\left(t=\varnothing ,1_{𝑜},\varnothing \right)\right)$$
14	12 13	syl	$$⊢t\in 2_{𝑜}\to A\left(t\right)=if\left(t=2_{𝑜},2_{𝑜},if\left(t=\varnothing ,1_{𝑜},\varnothing \right)\right)$$
15		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
16	15	onirri	$$⊢\neg 2_{𝑜}\in 2_{𝑜}$$
17		nelneq	$$⊢\left(t\in 2_{𝑜}\wedge \neg 2_{𝑜}\in 2_{𝑜}\right)\to \neg t=2_{𝑜}$$
18	16 17	mpan2	$$⊢t\in 2_{𝑜}\to \neg t=2_{𝑜}$$
19	18	iffalsed	$$⊢t\in 2_{𝑜}\to if\left(t=2_{𝑜},2_{𝑜},if\left(t=\varnothing ,1_{𝑜},\varnothing \right)\right)=if\left(t=\varnothing ,1_{𝑜},\varnothing \right)$$
20	14 19	eqtrd	$$⊢t\in 2_{𝑜}\to A\left(t\right)=if\left(t=\varnothing ,1_{𝑜},\varnothing \right)$$
21		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
22		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
23	21 22	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
24		0ex	$$⊢\varnothing \in \mathrm{V}$$
25	24	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
26	25 22	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
27	23 26	ifcli	$$⊢if\left(t=\varnothing ,1_{𝑜},\varnothing \right)\in 2_{𝑜}$$
28	20 27	eqeltrdi	$$⊢t\in 2_{𝑜}\to A\left(t\right)\in 2_{𝑜}$$
29	28	rgen	$$⊢\forall t\in 2_{𝑜}A\left(t\right)\in 2_{𝑜}$$
30		elelsuc	$$⊢\varnothing \in 2_{𝑜}\to \varnothing \in \mathrm{suc}{2}_{𝑜}$$
31	26 30	ax-mp	$$⊢\varnothing \in \mathrm{suc}{2}_{𝑜}$$
32	31 4	eleqtrri	$$⊢\varnothing \in 3_{𝑜}$$
33	1	parswapval	$$⊢\varnothing \in 3_{𝑜}\to A\left(\varnothing \right)=if\left(\varnothing =2_{𝑜},2_{𝑜},if\left(\varnothing =\varnothing ,1_{𝑜},\varnothing \right)\right)$$
34	32 33	ax-mp	$$⊢A\left(\varnothing \right)=if\left(\varnothing =2_{𝑜},2_{𝑜},if\left(\varnothing =\varnothing ,1_{𝑜},\varnothing \right)\right)$$
35		nelneq	$$⊢\left(\varnothing \in 2_{𝑜}\wedge \neg 2_{𝑜}\in 2_{𝑜}\right)\to \neg \varnothing =2_{𝑜}$$
36	26 16 35	mp2an	$$⊢\neg \varnothing =2_{𝑜}$$
37	36	iffalsei	$$⊢if\left(\varnothing =2_{𝑜},2_{𝑜},if\left(\varnothing =\varnothing ,1_{𝑜},\varnothing \right)\right)=if\left(\varnothing =\varnothing ,1_{𝑜},\varnothing \right)$$
38		eqid	$$⊢\varnothing =\varnothing$$
39	38	iftruei	$$⊢if\left(\varnothing =\varnothing ,1_{𝑜},\varnothing \right)=1_{𝑜}$$
40	34 37 39	3eqtri	$$⊢A\left(\varnothing \right)=1_{𝑜}$$
41	10 29 40	3pm3.2i	$$⊢\left(A\left(2_{𝑜}\right)=2_{𝑜}\wedge \forall t\in 2_{𝑜}A\left(t\right)\in 2_{𝑜}\wedge A\left(\varnothing \right)=1_{𝑜}\right)$$