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 =/= (/) /\ E. 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 e. _V
12 11 dmex
 |-  dom f e. _V
13 2 12 eqeltrrdi
 |-  ( f : A -onto-> B -> A e. _V )
14 fornex
 |-  ( A e. _V -> ( f : A -onto-> B -> B e. _V ) )
15 13 14 mpcom
 |-  ( f : A -onto-> B -> B e. _V )
16 0sdomg
 |-  ( B e. _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 e. _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 =/= (/) -> ( E. f f : A -onto-> B -> ( (/) ~< B /\ B ~<_ A ) ) )
25 24 imp
 |-  ( ( A =/= (/) /\ E. f f : A -onto-> B ) -> ( (/) ~< B /\ B ~<_ A ) )
26 sdomdomtr
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> (/) ~< A )
27 reldom
 |-  Rel ~<_
28 27 brrelex2i
 |-  ( B ~<_ A -> A e. _V )
29 28 adantl
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> A e. _V )
30 0sdomg
 |-  ( A e. _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 ) -> E. f f : A -onto-> B )
34 32 33 jca
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> ( A =/= (/) /\ E. f f : A -onto-> B ) )
35 25 34 impbii
 |-  ( ( A =/= (/) /\ E. f f : A -onto-> B ) <-> ( (/) ~< B /\ B ~<_ A ) )