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

Metamath Proof Explorer

Theorem mptcnv

Description: The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017)

Ref Expression
Hypothesis mptcnv.1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷 ) ) )
Assertion mptcnv ( 𝜑 → ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 mptcnv.1 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷 ) ) )
2 1 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷 ) } )
3 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
4 3 cnveqi ⊢ ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
5 cnvopab ⊢ ◡ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
6 4 5 eqtri ⊢ ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
7 df-mpt ⊢ ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷 ) }
8 2 6 7 3eqtr4g ⊢ ( 𝜑 → ◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐶 ↦ 𝐷 ) )