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

Metamath Proof Explorer

Theorem mpomptx

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x . (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypothesis mpompt.1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 )
Assertion mpomptx ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 )

Proof

Step Hyp Ref Expression
1 mpompt.1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 )
2 df-mpt ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝑤 = 𝐶 ) }
3 df-mpo ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) }
4 eliunxp ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
5 4 anbi1i ⊢ ( ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝑤 = 𝐶 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) )
6 19.41vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) )
7 anass ⊢ ( ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) )
8 1 eqeq2d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 = 𝐶 ↔ 𝑤 = 𝐷 ) )
9 8 anbi2d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) )
10 9 pm5.32i ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) )
11 7 10 bitri ⊢ ( ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) )
12 11 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑤 = 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) )
13 5 6 12 3bitr2i ⊢ ( ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝑤 = 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) )
14 13 opabbii ⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝑤 = 𝐶 ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) }
15 dfoprab2 ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) ) }
16 14 15 eqtr4i ⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝑤 = 𝐶 ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐷 ) }
17 3 16 eqtr4i ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝑤 = 𝐶 ) }
18 2 17 eqtr4i ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 )