# Metamath Proof Explorer

## Theorem dmmpossx

Description: The domain of a mapping is a subset of its base class. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypothesis fmpox.1 ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
Assertion dmmpossx ${⊢}\mathrm{dom}{F}\subseteq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 fmpox.1 ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
2 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}{B}$
3 nfcsb1v
4 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}{C}$
5 nfcv ${⊢}\underset{_}{Ⅎ}{v}\phantom{\rule{.4em}{0ex}}{C}$
6 nfcsb1v
7 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{u}$
8 nfcsb1v
9 7 8 nfcsbw
10 csbeq1a
11 csbeq1a
12 csbeq1a
13 11 12 sylan9eqr
14 2 3 4 5 6 9 10 13 cbvmpox
15 vex ${⊢}{u}\in \mathrm{V}$
16 vex ${⊢}{v}\in \mathrm{V}$
17 15 16 op1std ${⊢}{t}=⟨{u},{v}⟩\to {1}^{st}\left({t}\right)={u}$
18 17 csbeq1d
19 15 16 op2ndd ${⊢}{t}=⟨{u},{v}⟩\to {2}^{nd}\left({t}\right)={v}$
20 19 csbeq1d
21 20 csbeq2dv
22 18 21 eqtrd
23 22 mpomptx
24 14 1 23 3eqtr4i
25 24 dmmptss
26 nfcv ${⊢}\underset{_}{Ⅎ}{u}\phantom{\rule{.4em}{0ex}}\left(\left\{{x}\right\}×{B}\right)$
27 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{u}\right\}$
28 27 3 nfxp
29 sneq ${⊢}{x}={u}\to \left\{{x}\right\}=\left\{{u}\right\}$
30 29 10 xpeq12d
31 26 28 30 cbviun
32 25 31 sseqtrri ${⊢}\mathrm{dom}{F}\subseteq \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$