Metamath Proof Explorer

Theorem fodomfi2

Description: Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Assertion fodomfi2 
|- ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> B ~<_ A )

Proof

Step Hyp Ref Expression
1 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
2 1 3ad2ant3 
 |-  ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> F Fn A )
3 forn 
 |-  ( F : A -onto-> B -> ran F = B )
4 eqimss2 
 |-  ( ran F = B -> B C_ ran F )
5 3 4 syl 
 |-  ( F : A -onto-> B -> B C_ ran F )
6 5 3ad2ant3 
 |-  ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> B C_ ran F )
7 simp2 
 |-  ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> B e. Fin )
8 fipreima 
 |-  ( ( F Fn A /\ B C_ ran F /\ B e. Fin ) -> E. x e. ( ~P A i^i Fin ) ( F " x ) = B )
9 2 6 7 8 syl3anc 
 |-  ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> E. x e. ( ~P A i^i Fin ) ( F " x ) = B )
10 elinel2 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. Fin )
11 10 adantl 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
12 finnum 
 |-  ( x e. Fin -> x e. dom card )
13 11 12 syl 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> x e. dom card )
14 simpl3 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> F : A -onto-> B )
15 fofun 
 |-  ( F : A -onto-> B -> Fun F )
16 14 15 syl 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> Fun F )
17 elinel1 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
18 17 elpwid 
 |-  ( x e. ( ~P A i^i Fin ) -> x C_ A )
19 18 adantl 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> x C_ A )
20 fof 
 |-  ( F : A -onto-> B -> F : A --> B )
21 fdm 
 |-  ( F : A --> B -> dom F = A )
22 14 20 21 3syl 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> dom F = A )
23 19 22 sseqtrrd 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> x C_ dom F )
24 fores 
 |-  ( ( Fun F /\ x C_ dom F ) -> ( F |` x ) : x -onto-> ( F " x ) )
25 16 23 24 syl2anc 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> ( F |` x ) : x -onto-> ( F " x ) )
26 fodomnum 
 |-  ( x e. dom card -> ( ( F |` x ) : x -onto-> ( F " x ) -> ( F " x ) ~<_ x ) )
27 13 25 26 sylc 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> ( F " x ) ~<_ x )
28 simpl1 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> A e. V )
29 ssdomg 
 |-  ( A e. V -> ( x C_ A -> x ~<_ A ) )
30 28 19 29 sylc 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> x ~<_ A )
31 domtr 
 |-  ( ( ( F " x ) ~<_ x /\ x ~<_ A ) -> ( F " x ) ~<_ A )
32 27 30 31 syl2anc 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> ( F " x ) ~<_ A )
33 breq1 
 |-  ( ( F " x ) = B -> ( ( F " x ) ~<_ A <-> B ~<_ A ) )
34 32 33 syl5ibcom 
 |-  ( ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) /\ x e. ( ~P A i^i Fin ) ) -> ( ( F " x ) = B -> B ~<_ A ) )
35 34 rexlimdva 
 |-  ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> ( E. x e. ( ~P A i^i Fin ) ( F " x ) = B -> B ~<_ A ) )
36 9 35 mpd 
 |-  ( ( A e. V /\ B e. Fin /\ F : A -onto-> B ) -> B ~<_ A )