Metamath Proof Explorer

Theorem fin4en1

Description: Dedekind finite is a cardinal property. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion fin4en1 
|- ( A ~~ B -> ( A e. Fin4 -> B e. Fin4 ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( A ~~ B -> B ~~ A )
2 bren 
 |-  ( B ~~ A <-> E. f f : B -1-1-onto-> A )
3 simpr 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> x C. B )
4 f1of1 
 |-  ( f : B -1-1-onto-> A -> f : B -1-1-> A )
5 pssss 
 |-  ( x C. B -> x C_ B )
6 ssid 
 |-  B C_ B
7 5 6 jctir 
 |-  ( x C. B -> ( x C_ B /\ B C_ B ) )
8 f1imapss 
 |-  ( ( f : B -1-1-> A /\ ( x C_ B /\ B C_ B ) ) -> ( ( f " x ) C. ( f " B ) <-> x C. B ) )
9 4 7 8 syl2an 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> ( ( f " x ) C. ( f " B ) <-> x C. B ) )
10 3 9 mpbird 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> ( f " x ) C. ( f " B ) )
11 imadmrn 
 |-  ( f " dom f ) = ran f
12 f1odm 
 |-  ( f : B -1-1-onto-> A -> dom f = B )
13 12 imaeq2d 
 |-  ( f : B -1-1-onto-> A -> ( f " dom f ) = ( f " B ) )
14 dff1o5 
 |-  ( f : B -1-1-onto-> A <-> ( f : B -1-1-> A /\ ran f = A ) )
15 14 simprbi 
 |-  ( f : B -1-1-onto-> A -> ran f = A )
16 11 13 15 3eqtr3a 
 |-  ( f : B -1-1-onto-> A -> ( f " B ) = A )
17 16 adantr 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> ( f " B ) = A )
18 17 psseq2d 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> ( ( f " x ) C. ( f " B ) <-> ( f " x ) C. A ) )
19 10 18 mpbid 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> ( f " x ) C. A )
20 19 adantrr 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> ( f " x ) C. A )
21 vex 
 |-  x e. _V
22 21 f1imaen 
 |-  ( ( f : B -1-1-> A /\ x C_ B ) -> ( f " x ) ~~ x )
23 4 5 22 syl2an 
 |-  ( ( f : B -1-1-onto-> A /\ x C. B ) -> ( f " x ) ~~ x )
24 23 adantrr 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> ( f " x ) ~~ x )
25 simprr 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> x ~~ B )
26 entr 
 |-  ( ( ( f " x ) ~~ x /\ x ~~ B ) -> ( f " x ) ~~ B )
27 24 25 26 syl2anc 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> ( f " x ) ~~ B )
28 vex 
 |-  f e. _V
29 f1oen3g 
 |-  ( ( f e. _V /\ f : B -1-1-onto-> A ) -> B ~~ A )
30 28 29 mpan 
 |-  ( f : B -1-1-onto-> A -> B ~~ A )
31 30 adantr 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> B ~~ A )
32 entr 
 |-  ( ( ( f " x ) ~~ B /\ B ~~ A ) -> ( f " x ) ~~ A )
33 27 31 32 syl2anc 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> ( f " x ) ~~ A )
34 fin4i 
 |-  ( ( ( f " x ) C. A /\ ( f " x ) ~~ A ) -> -. A e. Fin4 )
35 20 33 34 syl2anc 
 |-  ( ( f : B -1-1-onto-> A /\ ( x C. B /\ x ~~ B ) ) -> -. A e. Fin4 )
36 35 ex 
 |-  ( f : B -1-1-onto-> A -> ( ( x C. B /\ x ~~ B ) -> -. A e. Fin4 ) )
37 36 exlimdv 
 |-  ( f : B -1-1-onto-> A -> ( E. x ( x C. B /\ x ~~ B ) -> -. A e. Fin4 ) )
38 37 con2d 
 |-  ( f : B -1-1-onto-> A -> ( A e. Fin4 -> -. E. x ( x C. B /\ x ~~ B ) ) )
39 38 exlimiv 
 |-  ( E. f f : B -1-1-onto-> A -> ( A e. Fin4 -> -. E. x ( x C. B /\ x ~~ B ) ) )
40 2 39 sylbi 
 |-  ( B ~~ A -> ( A e. Fin4 -> -. E. x ( x C. B /\ x ~~ B ) ) )
41 relen 
 |-  Rel ~~
42 41 brrelex1i 
 |-  ( B ~~ A -> B e. _V )
43 isfin4 
 |-  ( B e. _V -> ( B e. Fin4 <-> -. E. x ( x C. B /\ x ~~ B ) ) )
44 42 43 syl 
 |-  ( B ~~ A -> ( B e. Fin4 <-> -. E. x ( x C. B /\ x ~~ B ) ) )
45 40 44 sylibrd 
 |-  ( B ~~ A -> ( A e. Fin4 -> B e. Fin4 ) )
46 1 45 syl 
 |-  ( A ~~ B -> ( A e. Fin4 -> B e. Fin4 ) )