Metamath Proof Explorer

Theorem enfin2i

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

Ref Expression
Assertion enfin2i 
|- ( A ~~ B -> ( A e. Fin2 -> B e. Fin2 ) )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 elpwi 
 |-  ( x e. ~P ~P B -> x C_ ~P B )
3 imauni 
 |-  ( f " U. { y e. ~P A | ( f " y ) e. x } ) = U_ z e. { y e. ~P A | ( f " y ) e. x } ( f " z )
4 vex 
 |-  f e. _V
5 4 imaex 
 |-  ( f " z ) e. _V
6 5 dfiun2 
 |-  U_ z e. { y e. ~P A | ( f " y ) e. x } ( f " z ) = U. { w | E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) }
7 3 6 eqtri 
 |-  ( f " U. { y e. ~P A | ( f " y ) e. x } ) = U. { w | E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) }
8 imaeq2 
 |-  ( y = z -> ( f " y ) = ( f " z ) )
9 8 eleq1d 
 |-  ( y = z -> ( ( f " y ) e. x <-> ( f " z ) e. x ) )
10 9 rexrab 
 |-  ( E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) <-> E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) )
11 eleq1 
 |-  ( w = ( f " z ) -> ( w e. x <-> ( f " z ) e. x ) )
12 11 biimparc 
 |-  ( ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
13 12 rexlimivw 
 |-  ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
14 cnvimass 
 |-  ( `' f " w ) C_ dom f
15 f1odm 
 |-  ( f : A -1-1-onto-> B -> dom f = A )
16 15 ad3antrrr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> dom f = A )
17 14 16 sseqtrid 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> ( `' f " w ) C_ A )
18 4 cnvex 
 |-  `' f e. _V
19 18 imaex 
 |-  ( `' f " w ) e. _V
20 19 elpw 
 |-  ( ( `' f " w ) e. ~P A <-> ( `' f " w ) C_ A )
21 17 20 sylibr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> ( `' f " w ) e. ~P A )
22 f1ofo 
 |-  ( f : A -1-1-onto-> B -> f : A -onto-> B )
23 22 ad3antrrr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> f : A -onto-> B )
24 simprl 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> x C_ ~P B )
25 24 sselda 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> w e. ~P B )
26 25 elpwid 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> w C_ B )
27 foimacnv 
 |-  ( ( f : A -onto-> B /\ w C_ B ) -> ( f " ( `' f " w ) ) = w )
28 23 26 27 syl2anc 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> ( f " ( `' f " w ) ) = w )
29 28 eqcomd 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> w = ( f " ( `' f " w ) ) )
30 simpr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> w e. x )
31 29 30 eqeltrrd 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> ( f " ( `' f " w ) ) e. x )
32 imaeq2 
 |-  ( z = ( `' f " w ) -> ( f " z ) = ( f " ( `' f " w ) ) )
33 32 eleq1d 
 |-  ( z = ( `' f " w ) -> ( ( f " z ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
34 32 eqeq2d 
 |-  ( z = ( `' f " w ) -> ( w = ( f " z ) <-> w = ( f " ( `' f " w ) ) ) )
35 33 34 anbi12d 
 |-  ( z = ( `' f " w ) -> ( ( ( f " z ) e. x /\ w = ( f " z ) ) <-> ( ( f " ( `' f " w ) ) e. x /\ w = ( f " ( `' f " w ) ) ) ) )
36 35 rspcev 
 |-  ( ( ( `' f " w ) e. ~P A /\ ( ( f " ( `' f " w ) ) e. x /\ w = ( f " ( `' f " w ) ) ) ) -> E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) )
37 21 31 29 36 syl12anc 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) )
38 37 ex 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> ( w e. x -> E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) ) )
39 13 38 impbid2 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) <-> w e. x ) )
40 10 39 bitrid 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> ( E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) <-> w e. x ) )
41 40 eqabcdv 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> { w | E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) } = x )
42 41 unieqd 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> U. { w | E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) } = U. x )
43 7 42 eqtrid 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> ( f " U. { y e. ~P A | ( f " y ) e. x } ) = U. x )
44 simplr 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> A e. Fin2 )
45 ssrab2 
 |-  { y e. ~P A | ( f " y ) e. x } C_ ~P A
46 45 a1i 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> { y e. ~P A | ( f " y ) e. x } C_ ~P A )
47 simprrl 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> x =/= (/) )
48 n0 
 |-  ( x =/= (/) <-> E. w w e. x )
49 47 48 sylib 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> E. w w e. x )
50 imaeq2 
 |-  ( y = ( `' f " w ) -> ( f " y ) = ( f " ( `' f " w ) ) )
51 50 eleq1d 
 |-  ( y = ( `' f " w ) -> ( ( f " y ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
52 51 rspcev 
 |-  ( ( ( `' f " w ) e. ~P A /\ ( f " ( `' f " w ) ) e. x ) -> E. y e. ~P A ( f " y ) e. x )
53 21 31 52 syl2anc 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ w e. x ) -> E. y e. ~P A ( f " y ) e. x )
54 49 53 exlimddv 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> E. y e. ~P A ( f " y ) e. x )
55 rabn0 
 |-  ( { y e. ~P A | ( f " y ) e. x } =/= (/) <-> E. y e. ~P A ( f " y ) e. x )
56 54 55 sylibr 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> { y e. ~P A | ( f " y ) e. x } =/= (/) )
57 9 elrab 
 |-  ( z e. { y e. ~P A | ( f " y ) e. x } <-> ( z e. ~P A /\ ( f " z ) e. x ) )
58 imaeq2 
 |-  ( y = w -> ( f " y ) = ( f " w ) )
59 58 eleq1d 
 |-  ( y = w -> ( ( f " y ) e. x <-> ( f " w ) e. x ) )
60 59 elrab 
 |-  ( w e. { y e. ~P A | ( f " y ) e. x } <-> ( w e. ~P A /\ ( f " w ) e. x ) )
61 57 60 anbi12i 
 |-  ( ( z e. { y e. ~P A | ( f " y ) e. x } /\ w e. { y e. ~P A | ( f " y ) e. x } ) <-> ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) )
62 simprrr 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> [C.] Or x )
63 62 adantr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> [C.] Or x )
64 simprlr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( f " z ) e. x )
65 simprrr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( f " w ) e. x )
66 sorpssi 
 |-  ( ( [C.] Or x /\ ( ( f " z ) e. x /\ ( f " w ) e. x ) ) -> ( ( f " z ) C_ ( f " w ) \/ ( f " w ) C_ ( f " z ) ) )
67 63 64 65 66 syl12anc 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( ( f " z ) C_ ( f " w ) \/ ( f " w ) C_ ( f " z ) ) )
68 f1of1 
 |-  ( f : A -1-1-onto-> B -> f : A -1-1-> B )
69 68 ad3antrrr 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> f : A -1-1-> B )
70 simprll 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> z e. ~P A )
71 70 elpwid 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> z C_ A )
72 simprrl 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> w e. ~P A )
73 72 elpwid 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> w C_ A )
74 f1imass 
 |-  ( ( f : A -1-1-> B /\ ( z C_ A /\ w C_ A ) ) -> ( ( f " z ) C_ ( f " w ) <-> z C_ w ) )
75 69 71 73 74 syl12anc 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( ( f " z ) C_ ( f " w ) <-> z C_ w ) )
76 f1imass 
 |-  ( ( f : A -1-1-> B /\ ( w C_ A /\ z C_ A ) ) -> ( ( f " w ) C_ ( f " z ) <-> w C_ z ) )
77 69 73 71 76 syl12anc 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( ( f " w ) C_ ( f " z ) <-> w C_ z ) )
78 75 77 orbi12d 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( ( ( f " z ) C_ ( f " w ) \/ ( f " w ) C_ ( f " z ) ) <-> ( z C_ w \/ w C_ z ) ) )
79 67 78 mpbid 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( ( z e. ~P A /\ ( f " z ) e. x ) /\ ( w e. ~P A /\ ( f " w ) e. x ) ) ) -> ( z C_ w \/ w C_ z ) )
80 61 79 sylan2b 
 |-  ( ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) /\ ( z e. { y e. ~P A | ( f " y ) e. x } /\ w e. { y e. ~P A | ( f " y ) e. x } ) ) -> ( z C_ w \/ w C_ z ) )
81 80 ralrimivva 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> A. z e. { y e. ~P A | ( f " y ) e. x } A. w e. { y e. ~P A | ( f " y ) e. x } ( z C_ w \/ w C_ z ) )
82 sorpss 
 |-  ( [C.] Or { y e. ~P A | ( f " y ) e. x } <-> A. z e. { y e. ~P A | ( f " y ) e. x } A. w e. { y e. ~P A | ( f " y ) e. x } ( z C_ w \/ w C_ z ) )
83 81 82 sylibr 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> [C.] Or { y e. ~P A | ( f " y ) e. x } )
84 fin2i 
 |-  ( ( ( A e. Fin2 /\ { y e. ~P A | ( f " y ) e. x } C_ ~P A ) /\ ( { y e. ~P A | ( f " y ) e. x } =/= (/) /\ [C.] Or { y e. ~P A | ( f " y ) e. x } ) ) -> U. { y e. ~P A | ( f " y ) e. x } e. { y e. ~P A | ( f " y ) e. x } )
85 44 46 56 83 84 syl22anc 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> U. { y e. ~P A | ( f " y ) e. x } e. { y e. ~P A | ( f " y ) e. x } )
86 imaeq2 
 |-  ( z = U. { y e. ~P A | ( f " y ) e. x } -> ( f " z ) = ( f " U. { y e. ~P A | ( f " y ) e. x } ) )
87 86 eleq1d 
 |-  ( z = U. { y e. ~P A | ( f " y ) e. x } -> ( ( f " z ) e. x <-> ( f " U. { y e. ~P A | ( f " y ) e. x } ) e. x ) )
88 9 cbvrabv 
 |-  { y e. ~P A | ( f " y ) e. x } = { z e. ~P A | ( f " z ) e. x }
89 87 88 elrab2 
 |-  ( U. { y e. ~P A | ( f " y ) e. x } e. { y e. ~P A | ( f " y ) e. x } <-> ( U. { y e. ~P A | ( f " y ) e. x } e. ~P A /\ ( f " U. { y e. ~P A | ( f " y ) e. x } ) e. x ) )
90 89 simprbi 
 |-  ( U. { y e. ~P A | ( f " y ) e. x } e. { y e. ~P A | ( f " y ) e. x } -> ( f " U. { y e. ~P A | ( f " y ) e. x } ) e. x )
91 85 90 syl 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> ( f " U. { y e. ~P A | ( f " y ) e. x } ) e. x )
92 43 91 eqeltrrd 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [C.] Or x ) ) ) -> U. x e. x )
93 92 expr 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ x C_ ~P B ) -> ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) )
94 2 93 sylan2 
 |-  ( ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) /\ x e. ~P ~P B ) -> ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) )
95 94 ralrimiva 
 |-  ( ( f : A -1-1-onto-> B /\ A e. Fin2 ) -> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) )
96 95 ex 
 |-  ( f : A -1-1-onto-> B -> ( A e. Fin2 -> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
97 96 exlimiv 
 |-  ( E. f f : A -1-1-onto-> B -> ( A e. Fin2 -> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
98 1 97 sylbi 
 |-  ( A ~~ B -> ( A e. Fin2 -> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
99 relen 
 |-  Rel ~~
100 99 brrelex2i 
 |-  ( A ~~ B -> B e. _V )
101 isfin2 
 |-  ( B e. _V -> ( B e. Fin2 <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
102 100 101 syl 
 |-  ( A ~~ B -> ( B e. Fin2 <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
103 98 102 sylibrd 
 |-  ( A ~~ B -> ( A e. Fin2 -> B e. Fin2 ) )