Metamath Proof Explorer

Theorem enfin1ai

Description: Ia-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion enfin1ai 
|- ( A ~~ B -> ( A e. Fin1a -> B e. Fin1a ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( A ~~ B -> B ~~ A )
2 bren 
 |-  ( B ~~ A <-> E. f f : B -1-1-onto-> A )
3 1 2 sylib 
 |-  ( A ~~ B -> E. f f : B -1-1-onto-> A )
4 elpwi 
 |-  ( x e. ~P B -> x C_ B )
5 simplr 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> A e. Fin1a )
6 imassrn 
 |-  ( f " x ) C_ ran f
7 f1of 
 |-  ( f : B -1-1-onto-> A -> f : B --> A )
8 7 ad2antrr 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> f : B --> A )
9 8 frnd 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ran f C_ A )
10 6 9 sstrid 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( f " x ) C_ A )
11 fin1ai 
 |-  ( ( A e. Fin1a /\ ( f " x ) C_ A ) -> ( ( f " x ) e. Fin \/ ( A \ ( f " x ) ) e. Fin ) )
12 5 10 11 syl2anc 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( ( f " x ) e. Fin \/ ( A \ ( f " x ) ) e. Fin ) )
13 f1of1 
 |-  ( f : B -1-1-onto-> A -> f : B -1-1-> A )
14 13 ad2antrr 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> f : B -1-1-> A )
15 simpr 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> x C_ B )
16 vex 
 |-  x e. _V
17 16 a1i 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> x e. _V )
18 f1imaeng 
 |-  ( ( f : B -1-1-> A /\ x C_ B /\ x e. _V ) -> ( f " x ) ~~ x )
19 14 15 17 18 syl3anc 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( f " x ) ~~ x )
20 enfi 
 |-  ( ( f " x ) ~~ x -> ( ( f " x ) e. Fin <-> x e. Fin ) )
21 19 20 syl 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( ( f " x ) e. Fin <-> x e. Fin ) )
22 df-f1 
 |-  ( f : B -1-1-> A <-> ( f : B --> A /\ Fun `' f ) )
23 22 simprbi 
 |-  ( f : B -1-1-> A -> Fun `' f )
24 imadif 
 |-  ( Fun `' f -> ( f " ( B \ x ) ) = ( ( f " B ) \ ( f " x ) ) )
25 14 23 24 3syl 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( f " ( B \ x ) ) = ( ( f " B ) \ ( f " x ) ) )
26 f1ofo 
 |-  ( f : B -1-1-onto-> A -> f : B -onto-> A )
27 foima 
 |-  ( f : B -onto-> A -> ( f " B ) = A )
28 26 27 syl 
 |-  ( f : B -1-1-onto-> A -> ( f " B ) = A )
29 28 ad2antrr 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( f " B ) = A )
30 29 difeq1d 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( ( f " B ) \ ( f " x ) ) = ( A \ ( f " x ) ) )
31 25 30 eqtrd 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( f " ( B \ x ) ) = ( A \ ( f " x ) ) )
32 difssd 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( B \ x ) C_ B )
33 vex 
 |-  f e. _V
34 7 adantr 
 |-  ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) -> f : B --> A )
35 dmfex 
 |-  ( ( f e. _V /\ f : B --> A ) -> B e. _V )
36 33 34 35 sylancr 
 |-  ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) -> B e. _V )
37 36 adantr 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> B e. _V )
38 difexg 
 |-  ( B e. _V -> ( B \ x ) e. _V )
39 37 38 syl 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( B \ x ) e. _V )
40 f1imaeng 
 |-  ( ( f : B -1-1-> A /\ ( B \ x ) C_ B /\ ( B \ x ) e. _V ) -> ( f " ( B \ x ) ) ~~ ( B \ x ) )
41 14 32 39 40 syl3anc 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( f " ( B \ x ) ) ~~ ( B \ x ) )
42 31 41 eqbrtrrd 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( A \ ( f " x ) ) ~~ ( B \ x ) )
43 enfi 
 |-  ( ( A \ ( f " x ) ) ~~ ( B \ x ) -> ( ( A \ ( f " x ) ) e. Fin <-> ( B \ x ) e. Fin ) )
44 42 43 syl 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( ( A \ ( f " x ) ) e. Fin <-> ( B \ x ) e. Fin ) )
45 21 44 orbi12d 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( ( ( f " x ) e. Fin \/ ( A \ ( f " x ) ) e. Fin ) <-> ( x e. Fin \/ ( B \ x ) e. Fin ) ) )
46 12 45 mpbid 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x C_ B ) -> ( x e. Fin \/ ( B \ x ) e. Fin ) )
47 4 46 sylan2 
 |-  ( ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) /\ x e. ~P B ) -> ( x e. Fin \/ ( B \ x ) e. Fin ) )
48 47 ralrimiva 
 |-  ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) -> A. x e. ~P B ( x e. Fin \/ ( B \ x ) e. Fin ) )
49 isfin1a 
 |-  ( B e. _V -> ( B e. Fin1a <-> A. x e. ~P B ( x e. Fin \/ ( B \ x ) e. Fin ) ) )
50 36 49 syl 
 |-  ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) -> ( B e. Fin1a <-> A. x e. ~P B ( x e. Fin \/ ( B \ x ) e. Fin ) ) )
51 48 50 mpbird 
 |-  ( ( f : B -1-1-onto-> A /\ A e. Fin1a ) -> B e. Fin1a )
52 51 ex 
 |-  ( f : B -1-1-onto-> A -> ( A e. Fin1a -> B e. Fin1a ) )
53 52 exlimiv 
 |-  ( E. f f : B -1-1-onto-> A -> ( A e. Fin1a -> B e. Fin1a ) )
54 3 53 syl 
 |-  ( A ~~ B -> ( A e. Fin1a -> B e. Fin1a ) )