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

Metamath Proof Explorer

Theorem mpomptxf

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) (Revised by Thierry Arnoux, 31-Mar-2018)

Ref Expression
Hypotheses mpomptxf.0 ⊢ Ⅎ 𝑥 𝐶
mpomptxf.1 ⊢ Ⅎ 𝑦 𝐶
mpomptxf.2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 )
Assertion mpomptxf ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 )

Proof

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