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 ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
Assertion parswapval ⊢ U ∈ 3 𝑜 → A ⁡ U = if U = 2 𝑜 2 𝑜 if U = ∅ 1 𝑜 ∅

Proof

Step Hyp Ref Expression
1 parswapval.a ⊢ A = b ∈ 3 𝑜 ⟼ if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅
2 eqeq1 ⊢ b = U → b = 2 𝑜 ↔ U = 2 𝑜
3 eqeq1 ⊢ b = U → b = ∅ ↔ U = ∅
4 3 ifbid ⊢ b = U → if b = ∅ 1 𝑜 ∅ = if U = ∅ 1 𝑜 ∅
5 2 4 ifbieq2d ⊢ b = U → if b = 2 𝑜 2 𝑜 if b = ∅ 1 𝑜 ∅ = if U = 2 𝑜 2 𝑜 if U = ∅ 1 𝑜 ∅
6 2oex ⊢ 2 𝑜 ∈ V
7 1oex ⊢ 1 𝑜 ∈ V
8 0ex ⊢ ∅ ∈ V
9 7 8 ifex ⊢ if U = ∅ 1 𝑜 ∅ ∈ V
10 6 9 ifex ⊢ if U = 2 𝑜 2 𝑜 if U = ∅ 1 𝑜 ∅ ∈ V
11 5 1 10 fvmpt ⊢ U ∈ 3 𝑜 → A ⁡ U = if U = 2 𝑜 2 𝑜 if U = ∅ 1 𝑜 ∅