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

Metamath Proof Explorer

Theorem txswaphmeolem

Description: Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion txswaphmeolem ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( I ↾ ( 𝑋 × 𝑌 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
2 1 mpompt ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑧 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
3 mptresid ⊢ ( I ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑧 )
4 opelxpi ⊢ ( ( 𝑦 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
5 4 ancoms ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
6 5 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ⟨ 𝑦 , 𝑥 ⟩ ∈ ( 𝑌 × 𝑋 ) )
7 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) )
8 sneq ⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → { 𝑧 } = { ⟨ 𝑦 , 𝑥 ⟩ } )
9 8 cnveqd ⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → ◡ { 𝑧 } = ◡ { ⟨ 𝑦 , 𝑥 ⟩ } )
10 9 unieqd ⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → ∪ ◡ { 𝑧 } = ∪ ◡ { ⟨ 𝑦 , 𝑥 ⟩ } )
11 opswap ⊢ ∪ ◡ { ⟨ 𝑦 , 𝑥 ⟩ } = ⟨ 𝑥 , 𝑦 ⟩
12 10 11 eqtrdi ⊢ ( 𝑧 = ⟨ 𝑦 , 𝑥 ⟩ → ∪ ◡ { 𝑧 } = ⟨ 𝑥 , 𝑦 ⟩ )
13 12 mpompt ⊢ ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ∪ ◡ { 𝑧 } ) = ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
14 13 eqcomi ⊢ ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ∪ ◡ { 𝑧 } )
15 14 a1i ⊢ ( ⊤ → ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑧 ∈ ( 𝑌 × 𝑋 ) ↦ ∪ ◡ { 𝑧 } ) )
16 6 7 15 12 fmpoco ⊢ ( ⊤ → ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) )
17 16 mptru ⊢ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑥 , 𝑦 ⟩ )
18 2 3 17 3eqtr4ri ⊢ ( ( 𝑦 ∈ 𝑌 , 𝑥 ∈ 𝑋 ↦ ⟨ 𝑥 , 𝑦 ⟩ ) ∘ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝑦 , 𝑥 ⟩ ) ) = ( I ↾ ( 𝑋 × 𝑌 ) )