Metamath Proof Explorer

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 = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
Assertion parswapprop 
|- ( ( A ` 2o ) = 2o /\ A. t e. 2o ( A ` t ) e. 2o /\ ( A ` (/) ) = 1o )

Proof

Step Hyp Ref Expression
1 parswapval.a 
 |-  A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
2 2oex 
 |-  2o e. _V
3 2 sucid 
 |-  2o e. suc 2o
4 df-3o 
 |-  3o = suc 2o
5 3 4 eleqtrri 
 |-  2o e. 3o
6 1 parswapval 
 |-  ( 2o e. 3o -> ( A ` 2o ) = if ( 2o = 2o , 2o , if ( 2o = (/) , 1o , (/) ) ) )
7 5 6 ax-mp 
 |-  ( A ` 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 
 |-  ( A ` 2o ) = 2o
11 elelsuc 
 |-  ( t e. 2o -> t e. suc 2o )
12 11 4 eleqtrrdi 
 |-  ( t e. 2o -> t e. 3o )
13 1 parswapval 
 |-  ( t e. 3o -> ( A ` t ) = if ( t = 2o , 2o , if ( t = (/) , 1o , (/) ) ) )
14 12 13 syl 
 |-  ( t e. 2o -> ( A ` t ) = if ( t = 2o , 2o , if ( t = (/) , 1o , (/) ) ) )
15 2on 
 |-  2o e. On
16 15 onirri 
 |-  -. 2o e. 2o
17 nelneq 
 |-  ( ( t e. 2o /\ -. 2o e. 2o ) -> -. t = 2o )
18 16 17 mpan2 
 |-  ( t e. 2o -> -. t = 2o )
19 18 iffalsed 
 |-  ( t e. 2o -> if ( t = 2o , 2o , if ( t = (/) , 1o , (/) ) ) = if ( t = (/) , 1o , (/) ) )
20 14 19 eqtrd 
 |-  ( t e. 2o -> ( A ` t ) = if ( t = (/) , 1o , (/) ) )
21 1oelpr 
 |-  1o e. { (/) , 1o }
22 df2o3 
 |-  2o = { (/) , 1o }
23 21 22 eleqtrri 
 |-  1o e. 2o
24 0ex 
 |-  (/) e. _V
25 24 prid1 
 |-  (/) e. { (/) , 1o }
26 25 22 eleqtrri 
 |-  (/) e. 2o
27 23 26 ifcli 
 |-  if ( t = (/) , 1o , (/) ) e. 2o
28 20 27 eqeltrdi 
 |-  ( t e. 2o -> ( A ` t ) e. 2o )
29 28 rgen 
 |-  A. t e. 2o ( A ` t ) e. 2o
30 elelsuc 
 |-  ( (/) e. 2o -> (/) e. suc 2o )
31 26 30 ax-mp 
 |-  (/) e. suc 2o
32 31 4 eleqtrri 
 |-  (/) e. 3o
33 1 parswapval 
 |-  ( (/) e. 3o -> ( A ` (/) ) = if ( (/) = 2o , 2o , if ( (/) = (/) , 1o , (/) ) ) )
34 32 33 ax-mp 
 |-  ( A ` (/) ) = if ( (/) = 2o , 2o , if ( (/) = (/) , 1o , (/) ) )
35 nelneq 
 |-  ( ( (/) e. 2o /\ -. 2o e. 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 
 |-  ( A ` (/) ) = 1o
41 10 29 40 3pm3.2i 
 |-  ( ( A ` 2o ) = 2o /\ A. t e. 2o ( A ` t ) e. 2o /\ ( A ` (/) ) = 1o )