# Metamath Proof Explorer

## Theorem fodomb

Description: Equivalence of an onto mapping and dominance for a nonempty set. Proposition 10.35 of TakeutiZaring p. 93. (Contributed by NM, 29-Jul-2004)

Ref Expression
Assertion fodomb ${⊢}\left({A}\ne \varnothing \wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}\right)↔\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)$

### Proof

Step Hyp Ref Expression
1 fof ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to {f}:{A}⟶{B}$
2 1 fdmd ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \mathrm{dom}{f}={A}$
3 2 eqeq1d ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \left(\mathrm{dom}{f}=\varnothing ↔{A}=\varnothing \right)$
4 dm0rn0 ${⊢}\mathrm{dom}{f}=\varnothing ↔\mathrm{ran}{f}=\varnothing$
5 forn ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \mathrm{ran}{f}={B}$
6 5 eqeq1d ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \left(\mathrm{ran}{f}=\varnothing ↔{B}=\varnothing \right)$
7 4 6 syl5bb ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \left(\mathrm{dom}{f}=\varnothing ↔{B}=\varnothing \right)$
8 3 7 bitr3d ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \left({A}=\varnothing ↔{B}=\varnothing \right)$
9 8 necon3bid ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \left({A}\ne \varnothing ↔{B}\ne \varnothing \right)$
10 9 biimpac ${⊢}\left({A}\ne \varnothing \wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to {B}\ne \varnothing$
11 vex ${⊢}{f}\in \mathrm{V}$
12 11 dmex ${⊢}\mathrm{dom}{f}\in \mathrm{V}$
13 2 12 eqeltrrdi ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to {A}\in \mathrm{V}$
14 fornex ${⊢}{A}\in \mathrm{V}\to \left({f}:{A}\underset{onto}{⟶}{B}\to {B}\in \mathrm{V}\right)$
15 13 14 mpcom ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to {B}\in \mathrm{V}$
16 0sdomg ${⊢}{B}\in \mathrm{V}\to \left(\varnothing \prec {B}↔{B}\ne \varnothing \right)$
17 15 16 syl ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to \left(\varnothing \prec {B}↔{B}\ne \varnothing \right)$
18 17 adantl ${⊢}\left({A}\ne \varnothing \wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to \left(\varnothing \prec {B}↔{B}\ne \varnothing \right)$
19 10 18 mpbird ${⊢}\left({A}\ne \varnothing \wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to \varnothing \prec {B}$
20 19 ex ${⊢}{A}\ne \varnothing \to \left({f}:{A}\underset{onto}{⟶}{B}\to \varnothing \prec {B}\right)$
21 fodomg ${⊢}{A}\in \mathrm{V}\to \left({f}:{A}\underset{onto}{⟶}{B}\to {B}\preccurlyeq {A}\right)$
22 13 21 mpcom ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to {B}\preccurlyeq {A}$
23 20 22 jca2 ${⊢}{A}\ne \varnothing \to \left({f}:{A}\underset{onto}{⟶}{B}\to \left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\right)$
24 23 exlimdv ${⊢}{A}\ne \varnothing \to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}\to \left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\right)$
25 24 imp ${⊢}\left({A}\ne \varnothing \wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}\right)\to \left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)$
26 sdomdomtr ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to \varnothing \prec {A}$
27 reldom ${⊢}\mathrm{Rel}\preccurlyeq$
28 27 brrelex2i ${⊢}{B}\preccurlyeq {A}\to {A}\in \mathrm{V}$
29 28 adantl ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to {A}\in \mathrm{V}$
30 0sdomg ${⊢}{A}\in \mathrm{V}\to \left(\varnothing \prec {A}↔{A}\ne \varnothing \right)$
31 29 30 syl ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to \left(\varnothing \prec {A}↔{A}\ne \varnothing \right)$
32 26 31 mpbid ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to {A}\ne \varnothing$
33 fodomr ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}$
34 32 33 jca ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to \left({A}\ne \varnothing \wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}\right)$
35 25 34 impbii ${⊢}\left({A}\ne \varnothing \wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}\right)↔\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)$