This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 vex 
 |-  f e. _V
12 11 dmex 
 |-  dom f e. _V
13 2 12 eqeltrrdi 
 |-  ( f : A -onto-> B -> A e. _V )
14 focdmex 
 |-  ( 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 ) )