Metamath Proof Explorer

Theorem isinffi

Description: An infinite set contains subsets equinumerous to every finite set. Extension of isinf from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion isinffi 
|- ( ( -. A e. Fin /\ B e. Fin ) -> E. f f : B -1-1-> A )

Proof

Step Hyp Ref Expression
1 ficardom 
 |-  ( B e. Fin -> ( card ` B ) e. _om )
2 isinf 
 |-  ( -. A e. Fin -> A. a e. _om E. c ( c C_ A /\ c ~~ a ) )
3 breq2 
 |-  ( a = ( card ` B ) -> ( c ~~ a <-> c ~~ ( card ` B ) ) )
4 3 anbi2d 
 |-  ( a = ( card ` B ) -> ( ( c C_ A /\ c ~~ a ) <-> ( c C_ A /\ c ~~ ( card ` B ) ) ) )
5 4 exbidv 
 |-  ( a = ( card ` B ) -> ( E. c ( c C_ A /\ c ~~ a ) <-> E. c ( c C_ A /\ c ~~ ( card ` B ) ) ) )
6 5 rspcva 
 |-  ( ( ( card ` B ) e. _om /\ A. a e. _om E. c ( c C_ A /\ c ~~ a ) ) -> E. c ( c C_ A /\ c ~~ ( card ` B ) ) )
7 1 2 6 syl2anr 
 |-  ( ( -. A e. Fin /\ B e. Fin ) -> E. c ( c C_ A /\ c ~~ ( card ` B ) ) )
8 simprr 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> c ~~ ( card ` B ) )
9 ficardid 
 |-  ( B e. Fin -> ( card ` B ) ~~ B )
10 9 ad2antlr 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> ( card ` B ) ~~ B )
11 entr 
 |-  ( ( c ~~ ( card ` B ) /\ ( card ` B ) ~~ B ) -> c ~~ B )
12 8 10 11 syl2anc 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> c ~~ B )
13 12 ensymd 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> B ~~ c )
14 bren 
 |-  ( B ~~ c <-> E. f f : B -1-1-onto-> c )
15 13 14 sylib 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> E. f f : B -1-1-onto-> c )
16 f1of1 
 |-  ( f : B -1-1-onto-> c -> f : B -1-1-> c )
17 simplrl 
 |-  ( ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) /\ f : B -1-1-onto-> c ) -> c C_ A )
18 f1ss 
 |-  ( ( f : B -1-1-> c /\ c C_ A ) -> f : B -1-1-> A )
19 16 17 18 syl2an2 
 |-  ( ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) /\ f : B -1-1-onto-> c ) -> f : B -1-1-> A )
20 19 ex 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> ( f : B -1-1-onto-> c -> f : B -1-1-> A ) )
21 20 eximdv 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> ( E. f f : B -1-1-onto-> c -> E. f f : B -1-1-> A ) )
22 15 21 mpd 
 |-  ( ( ( -. A e. Fin /\ B e. Fin ) /\ ( c C_ A /\ c ~~ ( card ` B ) ) ) -> E. f f : B -1-1-> A )
23 7 22 exlimddv 
 |-  ( ( -. A e. Fin /\ B e. Fin ) -> E. f f : B -1-1-> A )