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	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 )