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

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 Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) Avoid ax-pow . (Revised by BTernaryTau, 23-Jun-2025)

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 0fi 
 |-  (/) e. Fin
28 sdomdomtrfi 
 |-  ( ( (/) e. Fin /\ (/) ~< B /\ B ~<_ A ) -> (/) ~< A )
29 27 28 mp3an1 
 |-  ( ( (/) ~< B /\ B ~<_ A ) -> (/) ~< A )
30 0sdomg 
 |-  ( A e. Fin -> ( (/) ~< A <-> A =/= (/) ) )
31 29 30 imbitrid 
 |-  ( A e. Fin -> ( ( (/) ~< B /\ B ~<_ A ) -> A =/= (/) ) )
32 fodomfir 
 |-  ( ( A e. Fin /\ (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B )
33 32 3expib 
 |-  ( A e. Fin -> ( ( (/) ~< B /\ B ~<_ A ) -> E. f f : A -onto-> B ) )
34 31 33 jcad 
 |-  ( A e. Fin -> ( ( (/) ~< B /\ B ~<_ A ) -> ( A =/= (/) /\ E. f f : A -onto-> B ) ) )
35 26 34 impbid 
 |-  ( A e. Fin -> ( ( A =/= (/) /\ E. f f : A -onto-> B ) <-> ( (/) ~< B /\ B ~<_ A ) ) )