Metamath Proof Explorer

Theorem iunxpf

Description: Indexed union on a Cartesian product equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008)

Ref Expression
Hypotheses iunxpf.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{C}$
iunxpf.2 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{C}$
iunxpf.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
iunxpf.4 ${⊢}{x}=⟨{y},{z}⟩\to {C}={D}$
Assertion iunxpf ${⊢}\bigcup _{{x}\in {A}×{B}}{C}=\bigcup _{{y}\in {A}}\bigcup _{{z}\in {B}}{D}$

Proof

Step Hyp Ref Expression
1 iunxpf.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{C}$
2 iunxpf.2 ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{C}$
3 iunxpf.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
4 iunxpf.4 ${⊢}{x}=⟨{y},{z}⟩\to {C}={D}$
5 1 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
6 2 nfcri ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}\in {C}$
7 3 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
8 4 eleq2d ${⊢}{x}=⟨{y},{z}⟩\to \left({w}\in {C}↔{w}\in {D}\right)$
9 5 6 7 8 rexxpf ${⊢}\exists {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{w}\in {C}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
10 eliun ${⊢}{w}\in \bigcup _{{x}\in {A}×{B}}{C}↔\exists {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{w}\in {C}$
11 eliun ${⊢}{w}\in \bigcup _{{y}\in {A}}\bigcup _{{z}\in {B}}{D}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{z}\in {B}}{D}$
12 eliun ${⊢}{w}\in \bigcup _{{z}\in {B}}{D}↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
13 12 rexbii ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{w}\in \bigcup _{{z}\in {B}}{D}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
14 11 13 bitri ${⊢}{w}\in \bigcup _{{y}\in {A}}\bigcup _{{z}\in {B}}{D}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
15 9 10 14 3bitr4i ${⊢}{w}\in \bigcup _{{x}\in {A}×{B}}{C}↔{w}\in \bigcup _{{y}\in {A}}\bigcup _{{z}\in {B}}{D}$
16 15 eqriv ${⊢}\bigcup _{{x}\in {A}×{B}}{C}=\bigcup _{{y}\in {A}}\bigcup _{{z}\in {B}}{D}$