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	⊢ 𝐴 = ( 𝑏 ∈ 3o ↦ if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) )
Assertion	parswapprop	⊢ ( ( 𝐴 ‘ 2o ) = 2o ∧ ∀ 𝑡 ∈ 2o ( 𝐴 ‘ 𝑡 ) ∈ 2o ∧ ( 𝐴 ‘ ∅ ) = 1o )

Proof

Step	Hyp	Ref	Expression
1		parswapval.a	⊢ 𝐴 = ( 𝑏 ∈ 3o ↦ if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) )
2		2oex	⊢ 2o ∈ V
3	2	sucid	⊢ 2o ∈ suc 2o
4		df-3o	⊢ 3o = suc 2o
5	3 4	eleqtrri	⊢ 2o ∈ 3o
6	1	parswapval	⊢ ( 2o ∈ 3o → ( 𝐴 ‘ 2o ) = if ( 2o = 2o , 2o , if ( 2o = ∅ , 1o , ∅ ) ) )
7	5 6	ax-mp	⊢ ( 𝐴 ‘ 2o ) = if ( 2o = 2o , 2o , if ( 2o = ∅ , 1o , ∅ ) )
8		eqid	⊢ 2o = 2o
9	8	iftruei	⊢ if ( 2o = 2o , 2o , if ( 2o = ∅ , 1o , ∅ ) ) = 2o
10	7 9	eqtri	⊢ ( 𝐴 ‘ 2o ) = 2o
11		elelsuc	⊢ ( 𝑡 ∈ 2o → 𝑡 ∈ suc 2o )
12	11 4	eleqtrrdi	⊢ ( 𝑡 ∈ 2o → 𝑡 ∈ 3o )
13	1	parswapval	⊢ ( 𝑡 ∈ 3o → ( 𝐴 ‘ 𝑡 ) = if ( 𝑡 = 2o , 2o , if ( 𝑡 = ∅ , 1o , ∅ ) ) )
14	12 13	syl	⊢ ( 𝑡 ∈ 2o → ( 𝐴 ‘ 𝑡 ) = if ( 𝑡 = 2o , 2o , if ( 𝑡 = ∅ , 1o , ∅ ) ) )
15		2on	⊢ 2o ∈ On
16	15	onirri	⊢ ¬ 2o ∈ 2o
17		nelneq	⊢ ( ( 𝑡 ∈ 2o ∧ ¬ 2o ∈ 2o ) → ¬ 𝑡 = 2o )
18	16 17	mpan2	⊢ ( 𝑡 ∈ 2o → ¬ 𝑡 = 2o )
19	18	iffalsed	⊢ ( 𝑡 ∈ 2o → if ( 𝑡 = 2o , 2o , if ( 𝑡 = ∅ , 1o , ∅ ) ) = if ( 𝑡 = ∅ , 1o , ∅ ) )
20	14 19	eqtrd	⊢ ( 𝑡 ∈ 2o → ( 𝐴 ‘ 𝑡 ) = if ( 𝑡 = ∅ , 1o , ∅ ) )
21		1oelpr	⊢ 1o ∈ { ∅ , 1o }
22		df2o3	⊢ 2o = { ∅ , 1o }
23	21 22	eleqtrri	⊢ 1o ∈ 2o
24		0ex	⊢ ∅ ∈ V
25	24	prid1	⊢ ∅ ∈ { ∅ , 1o }
26	25 22	eleqtrri	⊢ ∅ ∈ 2o
27	23 26	ifcli	⊢ if ( 𝑡 = ∅ , 1o , ∅ ) ∈ 2o
28	20 27	eqeltrdi	⊢ ( 𝑡 ∈ 2o → ( 𝐴 ‘ 𝑡 ) ∈ 2o )
29	28	rgen	⊢ ∀ 𝑡 ∈ 2o ( 𝐴 ‘ 𝑡 ) ∈ 2o
30		elelsuc	⊢ ( ∅ ∈ 2o → ∅ ∈ suc 2o )
31	26 30	ax-mp	⊢ ∅ ∈ suc 2o
32	31 4	eleqtrri	⊢ ∅ ∈ 3o
33	1	parswapval	⊢ ( ∅ ∈ 3o → ( 𝐴 ‘ ∅ ) = if ( ∅ = 2o , 2o , if ( ∅ = ∅ , 1o , ∅ ) ) )
34	32 33	ax-mp	⊢ ( 𝐴 ‘ ∅ ) = if ( ∅ = 2o , 2o , if ( ∅ = ∅ , 1o , ∅ ) )
35		nelneq	⊢ ( ( ∅ ∈ 2o ∧ ¬ 2o ∈ 2o ) → ¬ ∅ = 2o )
36	26 16 35	mp2an	⊢ ¬ ∅ = 2o
37	36	iffalsei	⊢ if ( ∅ = 2o , 2o , if ( ∅ = ∅ , 1o , ∅ ) ) = if ( ∅ = ∅ , 1o , ∅ )
38		eqid	⊢ ∅ = ∅
39	38	iftruei	⊢ if ( ∅ = ∅ , 1o , ∅ ) = 1o
40	34 37 39	3eqtri	⊢ ( 𝐴 ‘ ∅ ) = 1o
41	10 29 40	3pm3.2i	⊢ ( ( 𝐴 ‘ 2o ) = 2o ∧ ∀ 𝑡 ∈ 2o ( 𝐴 ‘ 𝑡 ) ∈ 2o ∧ ( 𝐴 ‘ ∅ ) = 1o )