MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  enfin2i Structured version   Unicode version
Theorem enfin2i 8718
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 7544 . . 3 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 elpwi 4024 . . . . . . 7 |- ( x e. ~P ~P B -> x C_ ~P B )
3 imauni 6159 . . . . . . . . . . 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 3112 . . . . . . . . . . . . 13 |- f e. _V
5 imaexg 6736 . . . . . . . . . . . . 13 |- ( f e. _V -> ( f " z ) e. _V )
64, 5ax-mp 5 . . . . . . . . . . . 12 |- ( f " z ) e. _V
76dfiun2 4366 . . . . . . . . . . 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 2486 . . . . . . . . . 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 5343 . . . . . . . . . . . . . . 15 |- ( y = z -> ( f " y ) = ( f " z ) )
109eleq1d 2526 . . . . . . . . . . . . . 14 |- ( y = z -> ( ( f " y ) e. x <-> ( f " z ) e. x ) )
1110rexrab 3263 . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . 16 |- ( w = ( f " z ) -> ( w e. x <-> ( f " z ) e. x ) )
1312biimparc 487 . . . . . . . . . . . . . . 15 |- ( ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
1413rexlimivw 2946 . . . . . . . . . . . . . 14 |- ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
15 cnvimass 5367 . . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) C_ dom f
16 f1odm 5826 . . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> B -> dom f = A )
1716ad3antrrr 729 . . . . . . . . . . . . . . . . . 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 3547 . . . . . . . . . . . . . . . . 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 6746 . . . . . . . . . . . . . . . . . . 19 |- `' f e. _V
20 imaexg 6736 . . . . . . . . . . . . . . . . . . 19 |- ( `' f e. _V -> ( `' f " w ) e. _V )
2119, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) e. _V
2221elpw 4021 . . . . . . . . . . . . . . . . 17 |- ( ( `' f " w ) e. ~P A <-> ( `' f " w ) C_ A )
2318, 22sylibr 212 . . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x C_ ~P B )
2726sselda 3499 . . . . . . . . . . . . . . . . . . . 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 4025 . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . 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 2465 . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . 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 2546 . . . . . . . . . . . . . . . 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 5343 . . . . . . . . . . . . . . . . . . 19 |- ( z = ( `' f " w ) -> ( f " z ) = ( f " ( `' f " w ) ) )
3534eleq1d 2526 . . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( ( f " z ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
3634eqeq2d 2471 . . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( w = ( f " z ) <-> w = ( f " ( `' f " w ) ) ) )
3735, 36anbi12d 710 . . . . . . . . . . . . . . . . 17 |- ( z = ( `' f " w ) -> ( ( ( f " z ) e. x /\ w = ( f " z ) ) <-> ( ( f " ( `' f " w ) ) e. x /\ w = ( f " ( `' f " w ) ) ) ) )
3837rspcev 3210 . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . 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 257 . . . . . . . . . . . 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 2595 . . . . . . . . . . 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 4261 . . . . . . . . . 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 2510 . . . . . . . . 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 755 . . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> A e. FinII )
47 ssrab2 3581 . . . . . . . . . . . 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 765 . . . . . . . . . . . . . 14 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x =/= (/) )
50 n0 3803 . . . . . . . . . . . . . 14 |- ( x =/= (/) <-> E. w w e. x )
5149, 50sylib 196 . . . . . . . . . . . . 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 5343 . . . . . . . . . . . . . . . 16 |- ( y = ( `' f " w ) -> ( f " y ) = ( f " ( `' f " w ) ) )
5352eleq1d 2526 . . . . . . . . . . . . . . 15 |- ( y = ( `' f " w ) -> ( ( f " y ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
5453rspcev 3210 . . . . . . . . . . . . . 14 |- ( ( ( `' f " w ) e. ~P A /\ ( f " ( `' f " w ) ) e. x ) -> E. y e. ~P A ( f " y ) e. x )
5523, 33, 54syl2anc 661 . . . . . . . . . . . . 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 1727 . . . . . . . . . . . 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 3814 . . . . . . . . . . . 12 |- ( { y e. ~P A | ( f " y ) e. x } =/= (/) <-> E. y e. ~P A ( f " y ) e. x )
5856, 57sylibr 212 . . . . . . . . . . 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 3257 . . . . . . . . . . . . . . 15 |- ( z e. { y e. ~P A | ( f " y ) e. x } <-> ( z e. ~P A /\ ( f " z ) e. x ) )
60 imaeq2 5343 . . . . . . . . . . . . . . . . 17 |- ( y = w -> ( f " y ) = ( f " w ) )
6160eleq1d 2526 . . . . . . . . . . . . . . . 16 |- ( y = w -> ( ( f " y ) e. x <-> ( f " w ) e. x ) )
6261elrab 3257 . . . . . . . . . . . . . . 15 |- ( w e. { y e. ~P A | ( f " y ) e. x } <-> ( w e. ~P A /\ ( f " w ) e. x ) )
6359, 62anbi12i 697 . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . . . 17 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> [ C.] Or x )
6564adantr 465 . . . . . . . . . . . . . . . 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 764 . . . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . . 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 6585 . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . 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 729 . . . . . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . . . . . 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 4025 . . . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . . . 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 4025 . . . . . . . . . . . . . . . . 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 6173 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( z C_ A /\ w C_ A ) ) -> ( ( f " z ) C_ ( f " w ) <-> z C_ w ) )
7771, 73, 75, 76syl12anc 1226 . . . . . . . . . . . . . . . 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 6173 . . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( w C_ A /\ z C_ A ) ) -> ( ( f " w ) C_ ( f " z ) <-> w C_ z ) )
7971, 75, 73, 78syl12anc 1226 . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . 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 2878 . . . . . . . . . . . 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 6584 . . . . . . . . . . . 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 212 . . . . . . . . . . 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 8692 . . . . . . . . . . 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 1229 . . . . . . . . . 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 5343 . . . . . . . . . . . . 13 |- ( z = U. { y e. ~P A | ( f " y ) e. x } -> ( f " z ) = ( f " U. { y e. ~P A | ( f " y ) e. x } ) )
8988eleq1d 2526 . . . . . . . . . . . 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 3108 . . . . . . . . . . . 12 |- { y e. ~P A | ( f " y ) e. x } = { z e. ~P A | ( f " z ) e. x }
9189, 90elrab2 3259 . . . . . . . . . . 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 464 . . . . . . . . . 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 16 . . . . . . . . 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 2546 . . . . . . . 8 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> U. x e. x )
9594expr 615 . . . . . . 7 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x C_ ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
962, 95sylan2 474 . . . . . 6 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x e. ~P ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
9796ralrimiva 2871 . . . . 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 434 . . . 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 1723 . . 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 195 . 2 |- ( A ~~ B -> ( A e. FinII -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
101 relen 7540 . . . 4 |- Rel ~~
102101brrelex2i 5050 . . 3 |- ( A ~~ B -> B e. _V )
103 isfin2 8691 . . 3 |- ( B e. _V -> ( B e. FinII <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
104102, 103syl 16 . 2 |- ( A ~~ B -> ( B e. FinII <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
105100, 104sylibrd 234 1 |- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1395   E.wex 1613   e. wcel 1819   {cab 2442   =/= wne 2652   A.wral 2807   E.wrex 2808   {crab 2811   _Vcvv 3109   C_ wss 3471   (/)c0 3793   ~Pcpw 4015   U.cuni 4251   U_ciun 4332   class class class wbr 4456   Or wor 4808   `'ccnv 5007   dom cdm 5008   "cima 5011   -1-1->wf1 5591   -onto->wfo 5592   -1-1-onto->wf1o 5593   [ C.] crpss 6578   ~~ cen 7532  FinIIcfin2 8676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-id 4804  df-po 4809  df-so 4810  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-rpss 6579  df-en 7536  df-fin2 8683
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator