MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  enfin2i Structured version   Unicode version
Theorem enfin2i 8740
Description: II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015.)
Assertion
Ref Expression
enfin2i |- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Proof of Theorem enfin2i
Dummy variables f w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bren 7577 . . 3 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 elpwi 3985 . . . . . . 7 |- ( x e. ~P ~P B -> x C_ ~P B )
3 imauni 6157 . . . . . . . . . . 11 |- ( 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 3081 . . . . . . . . . . . . 13 |- f e. _V
5 imaexg 6735 . . . . . . . . . . . . 13 |- ( f e. _V -> ( f " z ) e. _V )
64, 5ax-mp 5 . . . . . . . . . . . 12 |- ( f " z ) e. _V
76dfiun2 4327 . . . . . . . . . . 11 |- 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 ) }
83, 7eqtri 2449 . . . . . . . . . 10 |- ( 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 ) }
9 imaeq2 5175 . . . . . . . . . . . . . . 15 |- ( y = z -> ( f " y ) = ( f " z ) )
109eleq1d 2489 . . . . . . . . . . . . . 14 |- ( y = z -> ( ( f " y ) e. x <-> ( f " z ) e. x ) )
1110rexrab 3232 . . . . . . . . . . . . 13 |- ( 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 ) ) )
12 eleq1 2492 . . . . . . . . . . . . . . . 16 |- ( w = ( f " z ) -> ( w e. x <-> ( f " z ) e. x ) )
1312biimparc 489 . . . . . . . . . . . . . . 15 |- ( ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
1413rexlimivw 2912 . . . . . . . . . . . . . 14 |- ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
15 cnvimass 5199 . . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) C_ dom f
16 f1odm 5826 . . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> B -> dom f = A )
1716ad3antrrr 734 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> dom f = A )
1815, 17syl5sseq 3509 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> ( `' f " w ) C_ A )
194cnvex 6745 . . . . . . . . . . . . . . . . . . 19 |- `' f e. _V
20 imaexg 6735 . . . . . . . . . . . . . . . . . . 19 |- ( `' f e. _V -> ( `' f " w ) e. _V )
2119, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) e. _V
2221elpw 3982 . . . . . . . . . . . . . . . . 17 |- ( ( `' f " w ) e. ~P A <-> ( `' f " w ) C_ A )
2318, 22sylibr 215 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> ( `' f " w ) e. ~P A )
24 f1ofo 5829 . . . . . . . . . . . . . . . . . . . 20 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
2524ad3antrrr 734 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> f : A -onto-> B )
26 simprl 762 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x C_ ~P B )
2726sselda 3461 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> w e. ~P B )
2827elpwid 3986 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> w C_ B )
29 foimacnv 5839 . . . . . . . . . . . . . . . . . . 19 |- ( ( f : A -onto-> B /\ w C_ B ) -> ( f " ( `' f " w ) ) = w )
3025, 28, 29syl2anc 665 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> ( f " ( `' f " w ) ) = w )
3130eqcomd 2428 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> w = ( f " ( `' f " w ) ) )
32 simpr 462 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> w e. x )
3331, 32eqeltrrd 2509 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> ( f " ( `' f " w ) ) e. x )
34 imaeq2 5175 . . . . . . . . . . . . . . . . . . 19 |- ( z = ( `' f " w ) -> ( f " z ) = ( f " ( `' f " w ) ) )
3534eleq1d 2489 . . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( ( f " z ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
3634eqeq2d 2434 . . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( w = ( f " z ) <-> w = ( f " ( `' f " w ) ) ) )
3735, 36anbi12d 715 . . . . . . . . . . . . . . . . 17 |- ( z = ( `' f " w ) -> ( ( ( f " z ) e. x /\ w = ( f " z ) ) <-> ( ( f " ( `' f " w ) ) e. x /\ w = ( f " ( `' f " w ) ) ) ) )
3837rspcev 3179 . . . . . . . . . . . . . . . 16 |- ( ( ( `' 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 ) ) )
3923, 33, 31, 38syl12anc 1262 . . . . . . . . . . . . . . 15 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) )
4039ex 435 . . . . . . . . . . . . . 14 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> ( w e. x -> E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) ) )
4114, 40impbid2 207 . . . . . . . . . . . . 13 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) <-> w e. x ) )
4211, 41syl5bb 260 . . . . . . . . . . . 12 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) )
4342abbi1dv 2558 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> { w | E. z e. { y e. ~P A | ( f " y ) e. x } w = ( f " z ) } = x )
4443unieqd 4223 . . . . . . . . . 10 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
458, 44syl5eq 2473 . . . . . . . . 9 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> ( f " U. { y e. ~P A | ( f " y ) e. x } ) = U. x )
46 simplr 760 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> A e. FinII )
47 ssrab2 3543 . . . . . . . . . . . 12 |- { y e. ~P A | ( f " y ) e. x } C_ ~P A
4847a1i 11 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> { y e. ~P A | ( f " y ) e. x } C_ ~P A )
49 simprrl 772 . . . . . . . . . . . . . 14 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x =/= (/) )
50 n0 3768 . . . . . . . . . . . . . 14 |- ( x =/= (/) <-> E. w w e. x )
5149, 50sylib 199 . . . . . . . . . . . . 13 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> E. w w e. x )
52 imaeq2 5175 . . . . . . . . . . . . . . . 16 |- ( y = ( `' f " w ) -> ( f " y ) = ( f " ( `' f " w ) ) )
5352eleq1d 2489 . . . . . . . . . . . . . . 15 |- ( y = ( `' f " w ) -> ( ( f " y ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
5453rspcev 3179 . . . . . . . . . . . . . 14 |- ( ( ( `' f " w ) e. ~P A /\ ( f " ( `' f " w ) ) e. x ) -> E. y e. ~P A ( f " y ) e. x )
5523, 33, 54syl2anc 665 . . . . . . . . . . . . 13 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> E. y e. ~P A ( f " y ) e. x )
5651, 55exlimddv 1770 . . . . . . . . . . . 12 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> E. y e. ~P A ( f " y ) e. x )
57 rabn0 3779 . . . . . . . . . . . 12 |- ( { y e. ~P A | ( f " y ) e. x } =/= (/) <-> E. y e. ~P A ( f " y ) e. x )
5856, 57sylibr 215 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> { y e. ~P A | ( f " y ) e. x } =/= (/) )
5910elrab 3226 . . . . . . . . . . . . . . 15 |- ( z e. { y e. ~P A | ( f " y ) e. x } <-> ( z e. ~P A /\ ( f " z ) e. x ) )
60 imaeq2 5175 . . . . . . . . . . . . . . . . 17 |- ( y = w -> ( f " y ) = ( f " w ) )
6160eleq1d 2489 . . . . . . . . . . . . . . . 16 |- ( y = w -> ( ( f " y ) e. x <-> ( f " w ) e. x ) )
6261elrab 3226 . . . . . . . . . . . . . . 15 |- ( w e. { y e. ~P A | ( f " y ) e. x } <-> ( w e. ~P A /\ ( f " w ) e. x ) )
6359, 62anbi12i 701 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
64 simprrr 773 . . . . . . . . . . . . . . . . 17 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> [ C.] Or x )
6564adantr 466 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
66 simprlr 771 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
67 simprrr 773 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
68 sorpssi 6582 . . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or x /\ ( ( f " z ) e. x /\ ( f " w ) e. x ) ) -> ( ( f " z ) C_ ( f " w ) \/ ( f " w ) C_ ( f " z ) ) )
6965, 66, 67, 68syl12anc 1262 . . . . . . . . . . . . . . 15 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) ) )
70 f1of1 5821 . . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> B -> f : A -1-1-> B )
7170ad3antrrr 734 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
72 simprll 770 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
7372elpwid 3986 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
74 simprrl 772 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
7574elpwid 3986 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 )
76 f1imass 6171 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( z C_ A /\ w C_ A ) ) -> ( ( f " z ) C_ ( f " w ) <-> z C_ w ) )
7771, 73, 75, 76syl12anc 1262 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) )
78 f1imass 6171 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( w C_ A /\ z C_ A ) ) -> ( ( f " w ) C_ ( f " z ) <-> w C_ z ) )
7971, 75, 73, 78syl12anc 1262 . . . . . . . . . . . . . . . 16 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) )
8077, 79orbi12d 714 . . . . . . . . . . . . . . 15 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) ) )
8169, 80mpbid 213 . . . . . . . . . . . . . 14 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) )
8263, 81sylan2b 477 . . . . . . . . . . . . 13 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) )
8382ralrimivva 2844 . . . . . . . . . . . 12 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 ) )
84 sorpss 6581 . . . . . . . . . . . 12 |- ( [ 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 ) )
8583, 84sylibr 215 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> [ C.] Or { y e. ~P A | ( f " y ) e. x } )
86 fin2i 8714 . . . . . . . . . . 11 |- ( ( ( A e. FinII /\ { 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 } )
8746, 48, 58, 85, 86syl22anc 1265 . . . . . . . . . 10 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( 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 } )
88 imaeq2 5175 . . . . . . . . . . . . 13 |- ( z = U. { y e. ~P A | ( f " y ) e. x } -> ( f " z ) = ( f " U. { y e. ~P A | ( f " y ) e. x } ) )
8988eleq1d 2489 . . . . . . . . . . . 12 |- ( 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 ) )
9010cbvrabv 3077 . . . . . . . . . . . 12 |- { y e. ~P A | ( f " y ) e. x } = { z e. ~P A | ( f " z ) e. x }
9189, 90elrab2 3228 . . . . . . . . . . 11 |- ( 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 ) )
9291simprbi 465 . . . . . . . . . 10 |- ( 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 )
9387, 92syl 17 . . . . . . . . 9 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> ( f " U. { y e. ~P A | ( f " y ) e. x } ) e. x )
9445, 93eqeltrrd 2509 . . . . . . . 8 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> U. x e. x )
9594expr 618 . . . . . . 7 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x C_ ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
962, 95sylan2 476 . . . . . 6 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x e. ~P ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
9796ralrimiva 2837 . . . . 5 |- ( ( f : A -1-1-onto-> B /\ A e. FinII ) -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
9897ex 435 . . . 4 |- ( f : A -1-1-onto-> B -> ( A e. FinII -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
9998exlimiv 1766 . . 3 |- ( E. f f : A -1-1-onto-> B -> ( A e. FinII -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
1001, 99sylbi 198 . 2 |- ( A ~~ B -> ( A e. FinII -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
101 relen 7573 . . . 4 |- Rel ~~
102101brrelex2i 4887 . . 3 |- ( A ~~ B -> B e. _V )
103 isfin2 8713 . . 3 |- ( B e. _V -> ( B e. FinII <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
104102, 103syl 17 . 2 |- ( A ~~ B -> ( B e. FinII <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
105100, 104sylibrd 237 1 |- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1867   {cab 2405   =/= wne 2616   A.wral 2773   E.wrex 2774   {crab 2777   _Vcvv 3078   C_ wss 3433   (/)c0 3758   ~Pcpw 3976   U.cuni 4213   U_ciun 4293   class class class wbr 4417   Or wor 4765   `'ccnv 4844   dom cdm 4845   "cima 4848   -1-1->wf1 5589   -onto->wfo 5590   -1-1-onto->wf1o 5591   [ C.] crpss 6575   ~~ cen 7565  FinIIcfin2 8698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-iun 4295  df-br 4418  df-opab 4476  df-id 4760  df-po 4766  df-so 4767  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-rpss 6576  df-en 7569  df-fin2 8705
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator