# Metamath Proof Explorer

## Theorem elunirn

Description: Membership in the union of the range of a function. See elunirnALT for a shorter proof which uses ax-pow . (Contributed by NM, 24-Sep-2006)

Ref Expression
Assertion elunirn ${⊢}\mathrm{Fun}{F}\to \left({A}\in \bigcup \mathrm{ran}{F}↔\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eluni ${⊢}{A}\in \bigcup \mathrm{ran}{F}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)$
2 funfn ${⊢}\mathrm{Fun}{F}↔{F}Fn\mathrm{dom}{F}$
3 fvelrnb ${⊢}{F}Fn\mathrm{dom}{F}\to \left({y}\in \mathrm{ran}{F}↔\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)$
4 2 3 sylbi ${⊢}\mathrm{Fun}{F}\to \left({y}\in \mathrm{ran}{F}↔\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)$
5 4 anbi2d ${⊢}\mathrm{Fun}{F}\to \left(\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)↔\left({A}\in {y}\wedge \exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)\right)$
6 r19.42v ${⊢}\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {F}\left({x}\right)={y}\right)↔\left({A}\in {y}\wedge \exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)$
7 5 6 syl6bbr ${⊢}\mathrm{Fun}{F}\to \left(\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)↔\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {F}\left({x}\right)={y}\right)\right)$
8 eleq2 ${⊢}{F}\left({x}\right)={y}\to \left({A}\in {F}\left({x}\right)↔{A}\in {y}\right)$
9 8 biimparc ${⊢}\left({A}\in {y}\wedge {F}\left({x}\right)={y}\right)\to {A}\in {F}\left({x}\right)$
10 9 reximi ${⊢}\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {F}\left({x}\right)={y}\right)\to \exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)$
11 7 10 syl6bi ${⊢}\mathrm{Fun}{F}\to \left(\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)\to \exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)\right)$
12 11 exlimdv ${⊢}\mathrm{Fun}{F}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)\to \exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)\right)$
13 fvelrn ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to {F}\left({x}\right)\in \mathrm{ran}{F}$
14 13 a1d ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to \left({A}\in {F}\left({x}\right)\to {F}\left({x}\right)\in \mathrm{ran}{F}\right)$
15 14 ancld ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to \left({A}\in {F}\left({x}\right)\to \left({A}\in {F}\left({x}\right)\wedge {F}\left({x}\right)\in \mathrm{ran}{F}\right)\right)$
16 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
17 eleq2 ${⊢}{y}={F}\left({x}\right)\to \left({A}\in {y}↔{A}\in {F}\left({x}\right)\right)$
18 eleq1 ${⊢}{y}={F}\left({x}\right)\to \left({y}\in \mathrm{ran}{F}↔{F}\left({x}\right)\in \mathrm{ran}{F}\right)$
19 17 18 anbi12d ${⊢}{y}={F}\left({x}\right)\to \left(\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)↔\left({A}\in {F}\left({x}\right)\wedge {F}\left({x}\right)\in \mathrm{ran}{F}\right)\right)$
20 16 19 spcev ${⊢}\left({A}\in {F}\left({x}\right)\wedge {F}\left({x}\right)\in \mathrm{ran}{F}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)$
21 15 20 syl6 ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to \left({A}\in {F}\left({x}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)\right)$
22 21 rexlimdva ${⊢}\mathrm{Fun}{F}\to \left(\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)\right)$
23 12 22 impbid ${⊢}\mathrm{Fun}{F}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge {y}\in \mathrm{ran}{F}\right)↔\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)\right)$
24 1 23 syl5bb ${⊢}\mathrm{Fun}{F}\to \left({A}\in \bigcup \mathrm{ran}{F}↔\exists {x}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}{A}\in {F}\left({x}\right)\right)$