Theorem enfin2i 8486

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.

Step	Hyp	Ref	Expression
1		bren 7315	. . 3 |- ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2		elpwi 3866	. . . . . . 7 |- ( x e. ~P ~P B -> x C_ ~P B )
3		imauni 5960	. . . . . . . . . . 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 2973	. . . . . . . . . . . . 13 |- f e. _V
5		imaexg 6514	. . . . . . . . . . . . 13 |- ( f e. _V -> ( f " z ) e. _V )
6	4, 5	ax-mp 5	. . . . . . . . . . . 12 |- ( f " z ) e. _V
7	6	dfiun2 4201	. . . . . . . . . . 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 ) }
8	3, 7	eqtri 2461	. . . . . . . . . 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 5162	. . . . . . . . . . . . . . 15 |- ( y = z -> ( f " y ) = ( f " z ) )
10	9	eleq1d 2507	. . . . . . . . . . . . . 14 |- ( y = z -> ( ( f " y ) e. x <-> ( f " z ) e. x ) )
11	10	rexrab 3120	. . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . . 16 |- ( w = ( f " z ) -> ( w e. x <-> ( f " z ) e. x ) )
13	12	biimparc 484	. . . . . . . . . . . . . . 15 |- ( ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
14	13	rexlimivw 2835	. . . . . . . . . . . . . 14 |- ( E. z e. ~P A ( ( f " z ) e. x /\ w = ( f " z ) ) -> w e. x )
15		cnvimass 5186	. . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) C_ dom f
16		f1odm 5642	. . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> B -> dom f = A )
17	16	ad3antrrr 724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> dom f = A )
18	15, 17	syl5sseq 3401	. . . . . . . . . . . . . . . . 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 )
19	4	cnvex 6524	. . . . . . . . . . . . . . . . . . 19 |- `' f e. _V
20		imaexg 6514	. . . . . . . . . . . . . . . . . . 19 |- ( `' f e. _V -> ( `' f " w ) e. _V )
21	19, 20	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( `' f " w ) e. _V
22	21	elpw 3863	. . . . . . . . . . . . . . . . 17 |- ( ( `' f " w ) e. ~P A <-> ( `' f " w ) C_ A )
23	18, 22	sylibr 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 5645	. . . . . . . . . . . . . . . . . . . 20 |- ( f : A -1-1-onto-> B -> f : A -onto-> B )
25	24	ad3antrrr 724	. . . . . . . . . . . . . . . . . . 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 750	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x C_ ~P B )
27	26	sselda 3353	. . . . . . . . . . . . . . . . . . . 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 )
28	27	elpwid 3867	. . . . . . . . . . . . . . . . . . 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 5655	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : A -onto-> B /\ w C_ B ) -> ( f " ( `' f " w ) ) = w )
30	25, 28, 29	syl2anc 656	. . . . . . . . . . . . . . . . . 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 )
31	30	eqcomd 2446	. . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) /\ w e. x ) -> w e. x )
33	31, 32	eqeltrrd 2516	. . . . . . . . . . . . . . . 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 5162	. . . . . . . . . . . . . . . . . . 19 |- ( z = ( `' f " w ) -> ( f " z ) = ( f " ( `' f " w ) ) )
35	34	eleq1d 2507	. . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( ( f " z ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
36	34	eqeq2d 2452	. . . . . . . . . . . . . . . . . 18 |- ( z = ( `' f " w ) -> ( w = ( f " z ) <-> w = ( f " ( `' f " w ) ) ) )
37	35, 36	anbi12d 705	. . . . . . . . . . . . . . . . 17 |- ( z = ( `' f " w ) -> ( ( ( f " z ) e. x /\ w = ( f " z ) ) <-> ( ( f " ( `' f " w ) ) e. x /\ w = ( f " ( `' f " w ) ) ) ) )
38	37	rspcev 3070	. . . . . . . . . . . . . . . 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 ) ) )
39	23, 33, 31, 38	syl12anc 1211	. . . . . . . . . . . . . . 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 ) ) )
40	39	ex 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 ) ) ) )
41	14, 40	impbid2 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 ) )
42	11, 41	syl5bb 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 ) )
43	42	abbi1dv 2557	. . . . . . . . . . 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 )
44	43	unieqd 4098	. . . . . . . . . 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 )
45	8, 44	syl5eq 2485	. . . . . . . . 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 749	. . . . . . . . . . 11 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> A e. FinII )
47		ssrab2 3434	. . . . . . . . . . . 12 |- { y e. ~P A | ( f " y ) e. x } C_ ~P A
48	47	a1i 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 758	. . . . . . . . . . . . . 14 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> x =/= (/) )
50		n0 3643	. . . . . . . . . . . . . 14 |- ( x =/= (/) <-> E. w w e. x )
51	49, 50	sylib 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 5162	. . . . . . . . . . . . . . . 16 |- ( y = ( `' f " w ) -> ( f " y ) = ( f " ( `' f " w ) ) )
53	52	eleq1d 2507	. . . . . . . . . . . . . . 15 |- ( y = ( `' f " w ) -> ( ( f " y ) e. x <-> ( f " ( `' f " w ) ) e. x ) )
54	53	rspcev 3070	. . . . . . . . . . . . . 14 |- ( ( ( `' f " w ) e. ~P A /\ ( f " ( `' f " w ) ) e. x ) -> E. y e. ~P A ( f " y ) e. x )
55	23, 33, 54	syl2anc 656	. . . . . . . . . . . . 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 )
56	51, 55	exlimddv 1697	. . . . . . . . . . . 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 3654	. . . . . . . . . . . 12 |- ( { y e. ~P A | ( f " y ) e. x } =/= (/) <-> E. y e. ~P A ( f " y ) e. x )
58	56, 57	sylibr 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 } =/= (/) )
59	10	elrab 3114	. . . . . . . . . . . . . . 15 |- ( z e. { y e. ~P A | ( f " y ) e. x } <-> ( z e. ~P A /\ ( f " z ) e. x ) )
60		imaeq2 5162	. . . . . . . . . . . . . . . . 17 |- ( y = w -> ( f " y ) = ( f " w ) )
61	60	eleq1d 2507	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( ( f " y ) e. x <-> ( f " w ) e. x ) )
62	61	elrab 3114	. . . . . . . . . . . . . . 15 |- ( w e. { y e. ~P A | ( f " y ) e. x } <-> ( w e. ~P A /\ ( f " w ) e. x ) )
63	59, 62	anbi12i 692	. . . . . . . . . . . . . 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 759	. . . . . . . . . . . . . . . . 17 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> [ C.] Or x )
65	64	adantr 462	. . . . . . . . . . . . . . . 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 757	. . . . . . . . . . . . . . . 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 759	. . . . . . . . . . . . . . . 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 6365	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or x /\ ( ( f " z ) e. x /\ ( f " w ) e. x ) ) -> ( ( f " z ) C_ ( f " w ) \/ ( f " w ) C_ ( f " z ) ) )
69	65, 66, 67, 68	syl12anc 1211	. . . . . . . . . . . . . . 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 5637	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> B -> f : A -1-1-> B )
71	70	ad3antrrr 724	. . . . . . . . . . . . . . . . 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 756	. . . . . . . . . . . . . . . . . 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 )
73	72	elpwid 3867	. . . . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . . . . 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 )
75	74	elpwid 3867	. . . . . . . . . . . . . . . . 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 5974	. . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( z C_ A /\ w C_ A ) ) -> ( ( f " z ) C_ ( f " w ) <-> z C_ w ) )
77	71, 73, 75, 76	syl12anc 1211	. . . . . . . . . . . . . . . 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 5974	. . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-> B /\ ( w C_ A /\ z C_ A ) ) -> ( ( f " w ) C_ ( f " z ) <-> w C_ z ) )
79	71, 75, 73, 78	syl12anc 1211	. . . . . . . . . . . . . . . 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 ) )
80	77, 79	orbi12d 704	. . . . . . . . . . . . . . 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 ) ) )
81	69, 80	mpbid 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 ) )
82	63, 81	sylan2b 472	. . . . . . . . . . . . 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 ) )
83	82	ralrimivva 2806	. . . . . . . . . . . 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 6364	. . . . . . . . . . . 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 ) )
85	83, 84	sylibr 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 8460	. . . . . . . . . . 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 } )
87	46, 48, 58, 85, 86	syl22anc 1214	. . . . . . . . . 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 5162	. . . . . . . . . . . . 13 |- ( z = U. { y e. ~P A | ( f " y ) e. x } -> ( f " z ) = ( f " U. { y e. ~P A | ( f " y ) e. x } ) )
89	88	eleq1d 2507	. . . . . . . . . . . 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 ) )
90	10	cbvrabv 2969	. . . . . . . . . . . 12 |- { y e. ~P A | ( f " y ) e. x } = { z e. ~P A | ( f " z ) e. x }
91	89, 90	elrab2 3116	. . . . . . . . . . 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 ) )
92	91	simprbi 461	. . . . . . . . . 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 )
93	87, 92	syl 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 )
94	45, 93	eqeltrrd 2516	. . . . . . . 8 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ ( x C_ ~P B /\ ( x =/= (/) /\ [ C.] Or x ) ) ) -> U. x e. x )
95	94	expr 612	. . . . . . 7 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x C_ ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
96	2, 95	sylan2 471	. . . . . 6 |- ( ( ( f : A -1-1-onto-> B /\ A e. FinII ) /\ x e. ~P ~P B ) -> ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
97	96	ralrimiva 2797	. . . . 5 |- ( ( f : A -1-1-onto-> B /\ A e. FinII ) -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) )
98	97	ex 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 ) ) )
99	98	exlimiv 1693	. . 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 ) ) )
100	1, 99	sylbi 195	. 2 |- ( A ~~ B -> ( A e. FinII -> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
101		relen 7311	. . . 4 |- Rel ~~
102	101	brrelex2i 4876	. . 3 |- ( A ~~ B -> B e. _V )
103		isfin2 8459	. . 3 |- ( B e. _V -> ( B e. FinII <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
104	102, 103	syl 16	. 2 |- ( A ~~ B -> ( B e. FinII <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [ C.] Or x ) -> U. x e. x ) ) )
105	100, 104	sylibrd 234	1 |- ( A ~~ B -> ( A e. FinII -> B e. FinII ) )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1364   E.wex 1591   e. wcel 1761   {cab 2427   =/= wne 2604   A.wral 2713   E.wrex 2714   {crab 2717   _Vcvv 2970   C_ wss 3325   (/)c0 3634   ~Pcpw 3857   U.cuni 4088   U_ciun 4168   class class class wbr 4289   Or wor 4636   `'ccnv 4835   dom cdm 4836   "cima 4839   -1-1->wf1 5412   -onto->wfo 5413   -1-1-onto->wf1o 5414   [ C.] crpss 6358   ~~ cen 7303  Fin^IIcfin2 8444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-id 4632  df-po 4637  df-so 4638  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-rpss 6359  df-en 7307  df-fin2 8451

This theorem is referenced by: (None)