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 ${⊢}{z}=⟨{x},{y}⟩\to {C}={D}$
Assertion mpomptx ${⊢}\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)⟼{C}\right)=\left({x}\in {A},{y}\in {B}⟼{D}\right)$

Proof

Step Hyp Ref Expression
1 mpompt.1 ${⊢}{z}=⟨{x},{y}⟩\to {C}={D}$
2 df-mpt ${⊢}\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)⟼{C}\right)=\left\{⟨{z},{w}⟩|\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\wedge {w}={C}\right)\right\}$
3 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{D}\right)=\left\{⟨⟨{x},{y}⟩,{w}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right\}$
4 eliunxp ${⊢}{z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)$
5 4 anbi1i ${⊢}\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\wedge {w}={C}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {w}={C}\right)$
6 19.41vv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {w}={C}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {w}={C}\right)$
7 anass ${⊢}\left(\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {w}={C}\right)↔\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={C}\right)\right)$
8 1 eqeq2d ${⊢}{z}=⟨{x},{y}⟩\to \left({w}={C}↔{w}={D}\right)$
9 8 anbi2d ${⊢}{z}=⟨{x},{y}⟩\to \left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={C}\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)$
10 9 pm5.32i ${⊢}\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={C}\right)\right)↔\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)$
11 7 10 bitri ${⊢}\left(\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {w}={C}\right)↔\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)$
12 11 2exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\left({z}=⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\wedge {w}={C}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)$
13 5 6 12 3bitr2i ${⊢}\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\wedge {w}={C}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)$
14 13 opabbii ${⊢}\left\{⟨{z},{w}⟩|\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\wedge {w}={C}\right)\right\}=\left\{⟨{z},{w}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)\right\}$
15 dfoprab2 ${⊢}\left\{⟨⟨{x},{y}⟩,{w}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right\}=\left\{⟨{z},{w}⟩|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{x},{y}⟩\wedge \left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right)\right\}$
16 14 15 eqtr4i ${⊢}\left\{⟨{z},{w}⟩|\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\wedge {w}={C}\right)\right\}=\left\{⟨⟨{x},{y}⟩,{w}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {w}={D}\right)\right\}$
17 3 16 eqtr4i ${⊢}\left({x}\in {A},{y}\in {B}⟼{D}\right)=\left\{⟨{z},{w}⟩|\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\wedge {w}={C}\right)\right\}$
18 2 17 eqtr4i ${⊢}\left({z}\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)⟼{C}\right)=\left({x}\in {A},{y}\in {B}⟼{D}\right)$