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 Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) Avoid ax-pow . (Revised by BTernaryTau, 23-Jun-2025)

Ref Expression
Assertion fodomfib A Fin A f f : A onto B B B A

Proof

Step Hyp Ref Expression
1 fof f : A onto B f : A B
2 1 fdmd f : A onto B dom f = A
3 2 eqeq1d f : A onto B dom f = A =
4 dm0rn0 dom f = ran f =
5 forn f : A onto B ran f = B
6 5 eqeq1d f : A onto B ran f = B =
7 4 6 bitrid f : A onto B dom f = B =
8 3 7 bitr3d f : A onto B A = B =
9 8 necon3bid f : A onto B A B
10 9 biimpac A f : A onto B B
11 10 adantll A Fin A f : A onto B B
12 vex f V
13 12 rnex ran f V
14 5 13 eqeltrrdi f : A onto B B V
15 14 adantl A Fin f : A onto B B V
16 0sdomg B V B B
17 15 16 syl A Fin f : A onto B B B
18 17 adantlr A Fin A f : A onto B B B
19 11 18 mpbird A Fin A f : A onto B B
20 19 ex A Fin A f : A onto B B
21 fodomfi A Fin f : A onto B B A
22 21 ex A Fin f : A onto B B A
23 22 adantr A Fin A f : A onto B B A
24 20 23 jcad A Fin A f : A onto B B B A
25 24 exlimdv A Fin A f f : A onto B B B A
26 25 expimpd A Fin A f f : A onto B B B A
27 0fi Fin
28 sdomdomtrfi Fin B B A A
29 27 28 mp3an1 B B A A
30 0sdomg A Fin A A
31 29 30 imbitrid A Fin B B A A
32 fodomfir A Fin B B A f f : A onto B
33 32 3expib A Fin B B A f f : A onto B
34 31 33 jcad A Fin B B A A f f : A onto B
35 26 34 impbid A Fin A f f : A onto B B B A