Metamath Proof Explorer


Theorem mpomptx2

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version A ( y ) is not assumed to be constant w.r.t y , analogous to mpomptx . (Contributed by AV, 30-Mar-2019)

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

Proof

Step Hyp Ref Expression
1 mpomptx2.1 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐶 = 𝐷 )
2 df-mpt ( 𝑧 𝑦𝐵 ( 𝐴 × { 𝑦 } ) ↦ 𝐶 ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 𝑦𝐵 ( 𝐴 × { 𝑦 } ) ∧ 𝑤 = 𝐶 ) }
3 df-mpo ( 𝑥𝐴 , 𝑦𝐵𝐷 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∣ ( ( 𝑥𝐴𝑦𝐵 ) ∧ 𝑤 = 𝐷 ) }
4 eliunxp2 ( 𝑧 𝑦𝐵 ( 𝐴 × { 𝑦 } ) ↔ ∃ 𝑥𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )
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 ( 𝑧 𝑦𝐵 ( 𝐴 × { 𝑦 } ) ↦ 𝐶 ) = ( 𝑥𝐴 , 𝑦𝐵𝐷 )