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 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 syl5bb 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 vex f V
12 11 dmex dom f V
13 2 12 eqeltrrdi f : A onto B A V
14 fornex A V f : A onto B B V
15 13 14 mpcom f : A onto B B V
16 0sdomg B V B B
17 15 16 syl f : A onto B B B
18 17 adantl A f : A onto B B B
19 10 18 mpbird A f : A onto B B
20 19 ex A f : A onto B B
21 fodomg A V f : A onto B B A
22 13 21 mpcom f : A onto B B A
23 20 22 jca2 A f : A onto B B B A
24 23 exlimdv A f f : A onto B B B A
25 24 imp A f f : A onto B B B A
26 sdomdomtr B B A A
27 reldom Rel
28 27 brrelex2i B A A V
29 28 adantl B B A A V
30 0sdomg A V A A
31 29 30 syl B B A A A
32 26 31 mpbid B B A A
33 fodomr B B A f f : A onto B
34 32 33 jca B B A A f f : A onto B
35 25 34 impbii A f f : A onto B B B A