Metamath Proof Explorer

Theorem parswapval

Description: Evaluate the transposition of the two parallel-arrow values. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypothesis parswapval.a 
|- A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
Assertion parswapval 
|- ( U e. 3o -> ( A ` U ) = if ( U = 2o , 2o , if ( U = (/) , 1o , (/) ) ) )

Proof

Step Hyp Ref Expression
1 parswapval.a 
 |-  A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
2 eqeq1 
 |-  ( b = U -> ( b = 2o <-> U = 2o ) )
3 eqeq1 
 |-  ( b = U -> ( b = (/) <-> U = (/) ) )
4 3 ifbid 
 |-  ( b = U -> if ( b = (/) , 1o , (/) ) = if ( U = (/) , 1o , (/) ) )
5 2 4 ifbieq2d 
 |-  ( b = U -> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) = if ( U = 2o , 2o , if ( U = (/) , 1o , (/) ) ) )
6 2oex 
 |-  2o e. _V
7 1oex 
 |-  1o e. _V
8 0ex 
 |-  (/) e. _V
9 7 8 ifex 
 |-  if ( U = (/) , 1o , (/) ) e. _V
10 6 9 ifex 
 |-  if ( U = 2o , 2o , if ( U = (/) , 1o , (/) ) ) e. _V
11 5 1 10 fvmpt 
 |-  ( U e. 3o -> ( A ` U ) = if ( U = 2o , 2o , if ( U = (/) , 1o , (/) ) ) )