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 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 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 ) ) )