Theorem parswapval

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

	Ref	Expression
Hypothesis	parswapval.a	⊢ 𝐴 = ( 𝑏 ∈ 3o ↦ if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) )
Assertion	parswapval	⊢ ( 𝑈 ∈ 3o → ( 𝐴 ‘ 𝑈 ) = if ( 𝑈 = 2o , 2o , if ( 𝑈 = ∅ , 1o , ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		parswapval.a	⊢ 𝐴 = ( 𝑏 ∈ 3o ↦ if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) )
2		eqeq1	⊢ ( 𝑏 = 𝑈 → ( 𝑏 = 2o ↔ 𝑈 = 2o ) )
3		eqeq1	⊢ ( 𝑏 = 𝑈 → ( 𝑏 = ∅ ↔ 𝑈 = ∅ ) )
4	3	ifbid	⊢ ( 𝑏 = 𝑈 → if ( 𝑏 = ∅ , 1o , ∅ ) = if ( 𝑈 = ∅ , 1o , ∅ ) )
5	2 4	ifbieq2d	⊢ ( 𝑏 = 𝑈 → if ( 𝑏 = 2o , 2o , if ( 𝑏 = ∅ , 1o , ∅ ) ) = if ( 𝑈 = 2o , 2o , if ( 𝑈 = ∅ , 1o , ∅ ) ) )
6		2oex	⊢ 2o ∈ V
7		1oex	⊢ 1o ∈ V
8		0ex	⊢ ∅ ∈ V
9	7 8	ifex	⊢ if ( 𝑈 = ∅ , 1o , ∅ ) ∈ V
10	6 9	ifex	⊢ if ( 𝑈 = 2o , 2o , if ( 𝑈 = ∅ , 1o , ∅ ) ) ∈ V
11	5 1 10	fvmpt	⊢ ( 𝑈 ∈ 3o → ( 𝐴 ‘ 𝑈 ) = if ( 𝑈 = 2o , 2o , if ( 𝑈 = ∅ , 1o , ∅ ) ) )