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 e. Fin -> ( ( 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 10 adantll
 |-  ( ( ( A e. Fin /\ A =/= (/) ) /\ f : A -onto-> B ) -> B =/= (/) )
12 vex
 |-  f e. _V
13 12 rnex
 |-  ran f e. _V
14 5 13 eqeltrrdi
 |-  ( f : A -onto-> B -> B e. _V )
15 14 adantl
 |-  ( ( A e. Fin /\ f : A -onto-> B ) -> B e. _V )
16 0sdomg
 |-  ( B e. _V -> ( (/) ~< B <-> B =/= (/) ) )
17 15 16 syl
 |-  ( ( A e. Fin /\ f : A -onto-> B ) -> ( (/) ~< B <-> B =/= (/) ) )
18 17 adantlr
 |-  ( ( ( A e. Fin /\ A =/= (/) ) /\ f : A -onto-> B ) -> ( (/) ~< B <-> B =/= (/) ) )
19 11 18 mpbird
 |-  ( ( ( A e. Fin /\ A =/= (/) ) /\ f : A -onto-> B ) -> (/) ~< B )
20 19 ex
 |-  ( ( A e. Fin /\ A =/= (/) ) -> ( f : A -onto-> B -> (/) ~< B ) )
21 fodomfi
 |-  ( ( A e. Fin /\ f : A -onto-> B ) -> B ~<_ A )
22 21 ex
 |-  ( A e. Fin -> ( f : A -onto-> B -> B ~<_ A ) )
23 22 adantr
 |-  ( ( A e. Fin /\ A =/= (/) ) -> ( f : A -onto-> B -> B ~<_ A ) )
24 20 23 jcad
 |-  ( ( A e. Fin /\ A =/= (/) ) -> ( f : A -onto-> B -> ( (/) ~< B /\ B ~<_ A ) ) )
25 24 exlimdv
 |-  ( ( A e. Fin /\ A =/= (/) ) -> ( E. f f : A -onto-> B -> ( (/) ~< B /\ B ~<_ A ) ) )
26 25 expimpd
 |-  ( A e. Fin -> ( ( A =/= (/) /\ E. f f : A -onto-> B ) -> ( (/) ~< B /\ B ~<_ A ) ) )
27 sdomdomtr
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> (/) ~< A )
28 0sdomg
 |-  ( A e. Fin -> ( (/) ~< A <-> A =/= (/) ) )
29 27 28 syl5ib
 |-  ( A e. Fin -> ( ( (/) ~< B /\ B ~<_ A ) -> A =/= (/) ) )
30 fodomr
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )
31 29 30 jca2
 |-  ( A e. Fin -> ( ( (/) ~< B /\ B ~<_ A ) -> ( A =/= (/) /\ E. f f : A -onto-> B ) ) )
32 26 31 impbid
 |-  ( A e. Fin -> ( ( A =/= (/) /\ E. f f : A -onto-> B ) <-> ( (/) ~< B /\ B ~<_ A ) ) )