# Metamath Proof Explorer

## Theorem fodomfib

Description: Equivalence of an onto mapping and dominance for a nonempty finite set. Unlike fodomb for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006)

Ref Expression
Assertion fodomfib ${⊢}{A}\in \mathrm{Fin}\to \left(\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)\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 10 adantll ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to {B}\ne \varnothing$
12 vex ${⊢}{f}\in \mathrm{V}$
13 12 rnex ${⊢}\mathrm{ran}{f}\in \mathrm{V}$
14 5 13 syl6eqelr ${⊢}{f}:{A}\underset{onto}{⟶}{B}\to {B}\in \mathrm{V}$
15 14 adantl ${⊢}\left({A}\in \mathrm{Fin}\wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to {B}\in \mathrm{V}$
16 0sdomg ${⊢}{B}\in \mathrm{V}\to \left(\varnothing \prec {B}↔{B}\ne \varnothing \right)$
17 15 16 syl ${⊢}\left({A}\in \mathrm{Fin}\wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to \left(\varnothing \prec {B}↔{B}\ne \varnothing \right)$
18 17 adantlr ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to \left(\varnothing \prec {B}↔{B}\ne \varnothing \right)$
19 11 18 mpbird ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to \varnothing \prec {B}$
20 19 ex ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left({f}:{A}\underset{onto}{⟶}{B}\to \varnothing \prec {B}\right)$
21 fodomfi ${⊢}\left({A}\in \mathrm{Fin}\wedge {f}:{A}\underset{onto}{⟶}{B}\right)\to {B}\preccurlyeq {A}$
22 21 ex ${⊢}{A}\in \mathrm{Fin}\to \left({f}:{A}\underset{onto}{⟶}{B}\to {B}\preccurlyeq {A}\right)$
23 22 adantr ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left({f}:{A}\underset{onto}{⟶}{B}\to {B}\preccurlyeq {A}\right)$
24 20 23 jcad ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left({f}:{A}\underset{onto}{⟶}{B}\to \left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\right)$
25 24 exlimdv ${⊢}\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}\to \left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\right)$
26 25 expimpd ${⊢}{A}\in \mathrm{Fin}\to \left(\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)\right)$
27 sdomdomtr ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to \varnothing \prec {A}$
28 0sdomg ${⊢}{A}\in \mathrm{Fin}\to \left(\varnothing \prec {A}↔{A}\ne \varnothing \right)$
29 27 28 syl5ib ${⊢}{A}\in \mathrm{Fin}\to \left(\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to {A}\ne \varnothing \right)$
30 fodomr ${⊢}\left(\varnothing \prec {B}\wedge {B}\preccurlyeq {A}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{onto}{⟶}{B}$
31 29 30 jca2 ${⊢}{A}\in \mathrm{Fin}\to \left(\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)\right)$
32 26 31 impbid ${⊢}{A}\in \mathrm{Fin}\to \left(\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)\right)$