This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opswap

Description: Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008) (Revised by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion opswap ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴 ⟩

Proof

Step Hyp Ref Expression
1 cnvsng ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = { ⟨ 𝐵 , 𝐴 ⟩ } )
2 1 unieqd ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ∪ { ⟨ 𝐵 , 𝐴 ⟩ } )
3 opex ⊢ ⟨ 𝐵 , 𝐴 ⟩ ∈ V
4 3 unisn ⊢ ∪ { ⟨ 𝐵 , 𝐴 ⟩ } = ⟨ 𝐵 , 𝐴 ⟩
5 2 4 eqtrdi ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴 ⟩ )
6 uni0 ⊢ ∪ ∅ = ∅
7 opprc ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
8 7 sneqd ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { ⟨ 𝐴 , 𝐵 ⟩ } = { ∅ } )
9 8 cnveqd ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ◡ { ∅ } )
10 cnvsn0 ⊢ ◡ { ∅ } = ∅
11 9 10 eqtrdi ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ∅ )
12 11 unieqd ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ∪ ∅ )
13 ancom ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
14 opprc ⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ⟨ 𝐵 , 𝐴 ⟩ = ∅ )
15 13 14 sylnbi ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐵 , 𝐴 ⟩ = ∅ )
16 6 12 15 3eqtr4a ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴 ⟩ )
17 5 16 pm2.61i ⊢ ∪ ◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ⟨ 𝐵 , 𝐴 ⟩