MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  enfin2i Structured version   Visualization version   Unicode version
Theorem enfin2i 8748
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 7575 . . 3 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 elpwi 3959 . . . . . . 7 |- ( x e. ~P ~P B -> x C_ ~P B )
3 imauni 6149 . . . . . . . . . . 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 3047 . . . . . . . . . . . . 13 |- f e. _V
5 imaexg 6727 . . . . . . . . . . . . 13 |- ( f e. _V -> ( f " z ) e. _V )
64, 5ax-mp 5 . . . . . . . . . . . 12 |- ( f " z ) e. _V
76dfiun2 4311 . . . . . . . . . . 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 2472 . . . . . . . . . 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 5163 . . . . . . . . . . . . . . 15 |- ( y = z -> ( f " y ) = ( f " z ) )
109eleq1d 2512 . . . . . . . . . . . . . 14 |- ( y = z -> ( ( f " y ) e. x <-> ( f " z ) e. x ) )
1110rexrab 3201 . . . . . . . . . . . . 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 2516 . . . . . . . . . . . . . . . 16 |- ( w = ( f " z ) -> ( w e. x <-> ( f " z ) e. x ) )
1312biimparc 490 . . . . . . . . . . . . . . 15 |- ( ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
1413rexlimivw 2875 . . . . . . . . . . . . . 14 |- ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
15 cnvimass 5187 . . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) C_ dom f
16 f1odm 5816 . . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> B -> dom f = A )
1716ad3antrrr 735 . . . . . . . . . . . . . . . . . 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 3479 . . . . . . . . . . . . . . . . 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 6737 . . . . . . . . . . . . . . . . . . 19 |- `' f e. _V
20 imaexg 6727 . . . . . . . . . . . . . . . . . . 19 |- ( `' f e. _V -> ( `' f " w ) e. _V )
2119, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) e. _V
2221elpw 3956 . . . . . . . . . . . . . . . . 17 |- ( ( `' f " w ) e. ~P A <-> ( `' f " w ) C_ A )
2318, 22sylibr 216 . . . . . . . . . . . . . . . 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 5819 . . . . . . . . . . . . . . . . . . . 20 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
2524ad3antrrr 735 . . . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x C_ ~P B )
2726sselda 3431 . . . . . . . . . . . . . . . . . . . 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 3960 . . . . . . . . . . . . . . . . . . 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 5829 . . . . . . . . . . . . . . . . . . 19 |- ( ( f : A -onto-> B /\ w C_ B ) -> ( f " ( `' f " w ) ) = w )
3025, 28, 29syl2anc 666 . . . . . . . . . . . . . . . . . 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 2456 . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . 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 5163 . . . . . . . . . . . . . . . . . . 19 |- ( z = ( `' f " w ) -> ( f " z ) = ( f " ( `' f " w ) ) )
3534eleq1d 2512 . . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( ( f " z ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
3634eqeq2d 2460 . . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( w = ( f " z ) <-> w = ( f " ( `' f " w ) ) ) )
3735, 36anbi12d 716 . . . . . . . . . . . . . . . . 17 |- ( z = ( `' f " w ) -> ( ( ( f " z ) e. x /\ w = ( f " z ) ) <-> ( ( f " ( `' f " w ) ) e. x /\ w = ( f " ( `' f " w ) ) ) ) )
3837rspcev 3149 . . . . . . . . . . . . . . . 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 1265 . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . 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 208 . . . . . . . . . . . . 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 261 . . . . . . . . . . . 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 2570 . . . . . . . . . . 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 4207 . . . . . . . . . 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 2496 . . . . . . . . 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 761 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> A e. FinII )
47 ssrab2 3513 . . . . . . . . . . . 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 773 . . . . . . . . . . . . . 14 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x =/= (/) )
50 n0 3740 . . . . . . . . . . . . . 14 |- ( x =/= (/) <-> E. w w e. x )
5149, 50sylib 200 . . . . . . . . . . . . 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 5163 . . . . . . . . . . . . . . . 16 |- ( y = ( `' f " w ) -> ( f " y ) = ( f " ( `' f " w ) ) )
5352eleq1d 2512 . . . . . . . . . . . . . . 15 |- ( y = ( `' f " w ) -> ( ( f " y ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
5453rspcev 3149 . . . . . . . . . . . . . 14 |- ( ( ( `' f " w ) e. ~P A /\ ( f " ( `' f " w ) ) e. x ) -> E. y e. ~P A ( f " y ) e. x )
5523, 33, 54syl2anc 666 . . . . . . . . . . . . 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 1780 . . . . . . . . . . . 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 3751 . . . . . . . . . . . 12 |- ( { y e. ~P A | ( f " y ) e. x } =/= (/) <-> E. y e. ~P A ( f " y ) e. x )
5856, 57sylibr 216 . . . . . . . . . . 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 3195 . . . . . . . . . . . . . . 15 |- ( z e. { y e. ~P A | ( f " y ) e. x } <-> ( z e. ~P A /\ ( f " z ) e. x ) )
60 imaeq2 5163 . . . . . . . . . . . . . . . . 17 |- ( y = w -> ( f " y ) = ( f " w ) )
6160eleq1d 2512 . . . . . . . . . . . . . . . 16 |- ( y = w -> ( ( f " y ) e. x <-> ( f " w ) e. x ) )
6261elrab 3195 . . . . . . . . . . . . . . 15 |- ( w e. { y e. ~P A | ( f " y ) e. x } <-> ( w e. ~P A /\ ( f " w ) e. x ) )
6359, 62anbi12i 702 . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 17 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> [ C.] Or x )
6564adantr 467 . . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . 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 6574 . . . . . . . . . . . . . . . 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 1265 . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> B -> f : A -1-1-> B )
7170ad3antrrr 735 . . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . . . . 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 3960 . . . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . . 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 3960 . . . . . . . . . . . . . . . . 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 6163 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( z C_ A /\ w C_ A ) ) -> ( ( f " z ) C_ ( f " w ) <-> z C_ w ) )
7771, 73, 75, 76syl12anc 1265 . . . . . . . . . . . . . . . 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 6163 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( w C_ A /\ z C_ A ) ) -> ( ( f " w ) C_ ( f " z ) <-> w C_ z ) )
7971, 75, 73, 78syl12anc 1265 . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . 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 2808 . . . . . . . . . . . 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 6573 . . . . . . . . . . . 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 216 . . . . . . . . . . 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 8722 . . . . . . . . . . 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 1268 . . . . . . . . . 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 5163 . . . . . . . . . . . . 13 |- ( z = U. { y e. ~P A | ( f " y ) e. x } -> ( f " z ) = ( f " U. { y e. ~P A | ( f " y ) e. x } ) )
8988eleq1d 2512 . . . . . . . . . . . 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 3043 . . . . . . . . . . . 12 |- { y e. ~P A | ( f " y ) e. x } = { z e. ~P A | ( f " z ) e. x }
9189, 90elrab2 3197 . . . . . . . . . . 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 466 . . . . . . . . . 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 2529 . . . . . . . 8 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> U. x e. x )
9594expr 619 . . . . . . 7 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x C_ ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
962, 95sylan2 477 . . . . . 6 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x e. ~P ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
9796ralrimiva 2801 . . . . 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 436 . . . 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 1775 . . 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 199 . 2 |- ( A ~~ B -> ( A e. FinII -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
101 relen 7571 . . . 4 |- Rel ~~
102101brrelex2i 4875 . . 3 |- ( A ~~ B -> B e. _V )
103 isfin2 8721 . . 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 238 1 |- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   = wceq 1443   E.wex 1662   e. wcel 1886   {cab 2436   =/= wne 2621   A.wral 2736   E.wrex 2737   {crab 2740   _Vcvv 3044   C_ wss 3403   (/)c0 3730   ~Pcpw 3950   U.cuni 4197   U_ciun 4277   class class class wbr 4401   Or wor 4753   `'ccnv 4832   dom cdm 4833   "cima 4836   -1-1->wf1 5578   -onto->wfo 5579   -1-1-onto->wf1o 5580   [ C.] crpss 6567   ~~ cen 7563  FinIIcfin2 8706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-id 4748  df-po 4754  df-so 4755  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-rpss 6568  df-en 7567  df-fin2 8713
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator