Theorem fin1a2lem13 8840

Description: Lemma for fin1a2 8843. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

Assertion

Ref	Expression
fin1a2lem13	|- ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) -> -. ( B \ C ) e. FinII )

Proof of Theorem fin1a2lem13

Dummy variables e f g h x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 462	. . 3 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> ( B \ C ) e. FinII )
2		simpll1 1044	. . . 4 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> A C_ ~P B )
3		ssel2 3465	. . . . . . . . . 10 |- ( ( A C_ ~P B /\ g e. A ) -> g e. ~P B )
4	3	elpwid 3995	. . . . . . . . 9 |- ( ( A C_ ~P B /\ g e. A ) -> g C_ B )
5	4	ssdifd 3607	. . . . . . . 8 |- ( ( A C_ ~P B /\ g e. A ) -> ( g \ C ) C_ ( B \ C ) )
6		sseq1 3491	. . . . . . . 8 |- ( f = ( g \ C ) -> ( f C_ ( B \ C ) <-> ( g \ C ) C_ ( B \ C ) ) )
7	5, 6	syl5ibrcom 225	. . . . . . 7 |- ( ( A C_ ~P B /\ g e. A ) -> ( f = ( g \ C ) -> f C_ ( B \ C ) ) )
8	7	rexlimdva 2924	. . . . . 6 |- ( A C_ ~P B -> ( E. g e. A f = ( g \ C ) -> f C_ ( B \ C ) ) )
9		vex 3090	. . . . . . 7 |- f e. _V
10		eqid 2429	. . . . . . . 8 |- ( g e. A |-> ( g \ C ) ) = ( g e. A |-> ( g \ C ) )
11	10	elrnmpt 5101	. . . . . . 7 |- ( f e. _V -> ( f e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A f = ( g \ C ) ) )
12	9, 11	ax-mp 5	. . . . . 6 |- ( f e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A f = ( g \ C ) )
13		selpw 3992	. . . . . 6 |- ( f e. ~P ( B \ C ) <-> f C_ ( B \ C ) )
14	8, 12, 13	3imtr4g 273	. . . . 5 |- ( A C_ ~P B -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> f e. ~P ( B \ C ) ) )
15	14	ssrdv 3476	. . . 4 |- ( A C_ ~P B -> ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) )
16	2, 15	syl 17	. . 3 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) )
17		simplrr 769	. . . 4 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> C e. A )
18		difid 3869	. . . . . . 7 |- ( C \ C ) = (/)
19	18	eqcomi 2442	. . . . . 6 |- (/) = ( C \ C )
20		difeq1 3582	. . . . . . . 8 |- ( g = C -> ( g \ C ) = ( C \ C ) )
21	20	eqeq2d 2443	. . . . . . 7 |- ( g = C -> ( (/) = ( g \ C ) <-> (/) = ( C \ C ) ) )
22	21	rspcev 3188	. . . . . 6 |- ( ( C e. A /\ (/) = ( C \ C ) ) -> E. g e. A (/) = ( g \ C ) )
23	19, 22	mpan2 675	. . . . 5 |- ( C e. A -> E. g e. A (/) = ( g \ C ) )
24		0ex 4557	. . . . . 6 |- (/) e. _V
25	10	elrnmpt 5101	. . . . . 6 |- ( (/) e. _V -> ( (/) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A (/) = ( g \ C ) ) )
26	24, 25	ax-mp 5	. . . . 5 |- ( (/) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A (/) = ( g \ C ) )
27	23, 26	sylibr 215	. . . 4 |- ( C e. A -> (/) e. ran ( g e. A |-> ( g \ C ) ) )
28		ne0i 3773	. . . 4 |- ( (/) e. ran ( g e. A |-> ( g \ C ) ) -> ran ( g e. A |-> ( g \ C ) ) =/= (/) )
29	17, 27, 28	3syl 18	. . 3 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> ran ( g e. A |-> ( g \ C ) ) =/= (/) )
30		simpll2 1045	. . . 4 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> [ C.] Or A )
31		vex 3090	. . . . . . . 8 |- x e. _V
32	10	elrnmpt 5101	. . . . . . . 8 |- ( x e. _V -> ( x e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A x = ( g \ C ) ) )
33	31, 32	ax-mp 5	. . . . . . 7 |- ( x e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A x = ( g \ C ) )
34		difeq1 3582	. . . . . . . . . 10 |- ( g = e -> ( g \ C ) = ( e \ C ) )
35	34	eqeq2d 2443	. . . . . . . . 9 |- ( g = e -> ( x = ( g \ C ) <-> x = ( e \ C ) ) )
36	35	cbvrexv 3063	. . . . . . . 8 |- ( E. g e. A x = ( g \ C ) <-> E. e e. A x = ( e \ C ) )
37		sorpssi 6591	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( e C_ g \/ g C_ e ) )
38		ssdif 3606	. . . . . . . . . . . . . . . . 17 |- ( e C_ g -> ( e \ C ) C_ ( g \ C ) )
39		ssdif 3606	. . . . . . . . . . . . . . . . 17 |- ( g C_ e -> ( g \ C ) C_ ( e \ C ) )
40	38, 39	orim12i 518	. . . . . . . . . . . . . . . 16 |- ( ( e C_ g \/ g C_ e ) -> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) )
41	37, 40	syl 17	. . . . . . . . . . . . . . 15 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) )
42		sseq2 3492	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( ( e \ C ) C_ f <-> ( e \ C ) C_ ( g \ C ) ) )
43		sseq1 3491	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( f C_ ( e \ C ) <-> ( g \ C ) C_ ( e \ C ) ) )
44	42, 43	orbi12d 714	. . . . . . . . . . . . . . 15 |- ( f = ( g \ C ) -> ( ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) <-> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) ) )
45	41, 44	syl5ibrcom 225	. . . . . . . . . . . . . 14 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
46	45	expr 618	. . . . . . . . . . . . 13 |- ( ( [ C.] Or A /\ e e. A ) -> ( g e. A -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) ) )
47	46	rexlimdv 2922	. . . . . . . . . . . 12 |- ( ( [ C.] Or A /\ e e. A ) -> ( E. g e. A f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
48	12, 47	syl5bi 220	. . . . . . . . . . 11 |- ( ( [ C.] Or A /\ e e. A ) -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
49	48	ralrimiv 2844	. . . . . . . . . 10 |- ( ( [ C.] Or A /\ e e. A ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) )
50		sseq1 3491	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( x C_ f <-> ( e \ C ) C_ f ) )
51		sseq2 3492	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( f C_ x <-> f C_ ( e \ C ) ) )
52	50, 51	orbi12d 714	. . . . . . . . . . 11 |- ( x = ( e \ C ) -> ( ( x C_ f \/ f C_ x ) <-> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
53	52	ralbidv 2871	. . . . . . . . . 10 |- ( x = ( e \ C ) -> ( A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) <-> A. f e. ran ( g e. A |-> ( g \ C ) ) ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
54	49, 53	syl5ibrcom 225	. . . . . . . . 9 |- ( ( [ C.] Or A /\ e e. A ) -> ( x = ( e \ C ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
55	54	rexlimdva 2924	. . . . . . . 8 |- ( [ C.] Or A -> ( E. e e. A x = ( e \ C ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
56	36, 55	syl5bi 220	. . . . . . 7 |- ( [ C.] Or A -> ( E. g e. A x = ( g \ C ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
57	33, 56	syl5bi 220	. . . . . 6 |- ( [ C.] Or A -> ( x e. ran ( g e. A |-> ( g \ C ) ) -> A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) ) )
58	57	ralrimiv 2844	. . . . 5 |- ( [ C.] Or A -> A. x e. ran ( g e. A |-> ( g \ C ) ) A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) )
59		sorpss 6590	. . . . 5 |- ( [ C.] Or ran ( g e. A |-> ( g \ C ) ) <-> A. x e. ran ( g e. A |-> ( g \ C ) ) A. f e. ran ( g e. A |-> ( g \ C ) ) ( x C_ f \/ f C_ x ) )
60	58, 59	sylibr 215	. . . 4 |- ( [ C.] Or A -> [ C.] Or ran ( g e. A |-> ( g \ C ) ) )
61	30, 60	syl 17	. . 3 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> [ C.] Or ran ( g e. A |-> ( g \ C ) ) )
62		fin2i 8723	. . 3 |- ( ( ( ( B \ C ) e. FinII /\ ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) ) /\ ( ran ( g e. A |-> ( g \ C ) ) =/= (/) /\ [ C.] Or ran ( g e. A |-> ( g \ C ) ) ) ) -> U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) )
63	1, 16, 29, 61, 62	syl22anc 1265	. 2 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) )
64		simpll3 1046	. . 3 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> -. U. A e. A )
65		difeq1 3582	. . . . . . 7 |- ( g = f -> ( g \ C ) = ( f \ C ) )
66	65	cbvmptv 4518	. . . . . 6 |- ( g e. A |-> ( g \ C ) ) = ( f e. A |-> ( f \ C ) )
67	66	elrnmpt 5101	. . . . 5 |- ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) -> ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. f e. A U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) )
68	67	ibi 244	. . . 4 |- ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) -> E. f e. A U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
69		eqid 2429	. . . . . . . . . . . . . . . 16 |- ( h \ C ) = ( h \ C )
70		difeq1 3582	. . . . . . . . . . . . . . . . . 18 |- ( g = h -> ( g \ C ) = ( h \ C ) )
71	70	eqeq2d 2443	. . . . . . . . . . . . . . . . 17 |- ( g = h -> ( ( h \ C ) = ( g \ C ) <-> ( h \ C ) = ( h \ C ) ) )
72	71	rspcev 3188	. . . . . . . . . . . . . . . 16 |- ( ( h e. A /\ ( h \ C ) = ( h \ C ) ) -> E. g e. A ( h \ C ) = ( g \ C ) )
73	69, 72	mpan2 675	. . . . . . . . . . . . . . 15 |- ( h e. A -> E. g e. A ( h \ C ) = ( g \ C ) )
74	73	adantl 467	. . . . . . . . . . . . . 14 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> E. g e. A ( h \ C ) = ( g \ C ) )
75		vex 3090	. . . . . . . . . . . . . . 15 |- h e. _V
76		difexg 4573	. . . . . . . . . . . . . . 15 |- ( h e. _V -> ( h \ C ) e. _V )
77	10	elrnmpt 5101	. . . . . . . . . . . . . . 15 |- ( ( h \ C ) e. _V -> ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( h \ C ) = ( g \ C ) ) )
78	75, 76, 77	mp2b 10	. . . . . . . . . . . . . 14 |- ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( h \ C ) = ( g \ C ) )
79	74, 78	sylibr 215	. . . . . . . . . . . . 13 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
80		elssuni 4251	. . . . . . . . . . . . 13 |- ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) -> ( h \ C ) C_ U. ran ( g e. A |-> ( g \ C ) ) )
81	79, 80	syl 17	. . . . . . . . . . . 12 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ U. ran ( g e. A |-> ( g \ C ) ) )
82		simplr 760	. . . . . . . . . . . 12 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
83	81, 82	sseqtrd 3506	. . . . . . . . . . 11 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
84	83	adantll 718	. . . . . . . . . 10 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
85		unss2 3643	. . . . . . . . . . 11 |- ( ( h \ C ) C_ ( f \ C ) -> ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) )
86		uncom 3616	. . . . . . . . . . . . . . 15 |- ( C u. ( h \ C ) ) = ( ( h \ C ) u. C )
87		undif1 3876	. . . . . . . . . . . . . . 15 |- ( ( h \ C ) u. C ) = ( h u. C )
88	86, 87	eqtri 2458	. . . . . . . . . . . . . 14 |- ( C u. ( h \ C ) ) = ( h u. C )
89	88	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( C u. ( h \ C ) ) = ( h u. C ) )
90	64	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> -. U. A e. A )
91	17	ad2antrr 730	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> C e. A )
92		simplrr 769	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
93		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x \ C ) = ( x \ C )
94		difeq1 3582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( g = x -> ( g \ C ) = ( x \ C ) )
95	94	eqeq2d 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( g = x -> ( ( x \ C ) = ( g \ C ) <-> ( x \ C ) = ( x \ C ) ) )
96	95	rspcev 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A /\ ( x \ C ) = ( x \ C ) ) -> E. g e. A ( x \ C ) = ( g \ C ) )
97	93, 96	mpan2 675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. A -> E. g e. A ( x \ C ) = ( g \ C ) )
98		difexg 4573	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. _V -> ( x \ C ) e. _V )
99	10	elrnmpt 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x \ C ) e. _V -> ( ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( x \ C ) = ( g \ C ) ) )
100	31, 98, 99	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A ( x \ C ) = ( g \ C ) )
101	97, 100	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. A -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
102	101	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
103		simpllr 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) )
104		ssdif0 3857	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f C_ C <-> ( f \ C ) = (/) )
105	104	biimpi 197	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f C_ C -> ( f \ C ) = (/) )
106	105	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( f \ C ) = (/) )
107	103, 106	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> U. ran ( g e. A |-> ( g \ C ) ) = (/) )
108		uni0c 4248	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( U. ran ( g e. A |-> ( g \ C ) ) = (/) <-> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
109	107, 108	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
110		eqeq1 2433	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( e = ( x \ C ) -> ( e = (/) <-> ( x \ C ) = (/) ) )
111	110	rspcva 3186	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) /\ A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) ) -> ( x \ C ) = (/) )
112	102, 109, 111	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) = (/) )
113		ssdif0 3857	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x C_ C <-> ( x \ C ) = (/) )
114	112, 113	sylibr 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> x C_ C )
115	114	ralrimiva 2846	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> A. x e. A x C_ C )
116		unissb 4253	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. A C_ C <-> A. x e. A x C_ C )
117	115, 116	sylibr 215	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A C_ C )
118		elssuni 4251	. . . . . . . . . . . . . . . . . . . . 21 |- ( C e. A -> C C_ U. A )
119	118	ad2antrr 730	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C C_ U. A )
120	117, 119	eqssd 3487	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A = C )
121		simpll 758	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C e. A )
122	120, 121	eqeltrd 2517	. . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A e. A )
123	122	ex 435	. . . . . . . . . . . . . . . . 17 |- ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) -> ( f C_ C -> U. A e. A ) )
124	91, 92, 123	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( f C_ C -> U. A e. A ) )
125	90, 124	mtod 180	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> -. f C_ C )
126	30	ad2antrr 730	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> [ C.] Or A )
127		simplrl 768	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> f e. A )
128		sorpssi 6591	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( f e. A /\ C e. A ) ) -> ( f C_ C \/ C C_ f ) )
129	126, 127, 91, 128	syl12anc 1262	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( f C_ C \/ C C_ f ) )
130		orel1 383	. . . . . . . . . . . . . . 15 |- ( -. f C_ C -> ( ( f C_ C \/ C C_ f ) -> C C_ f ) )
131	125, 129, 130	sylc 62	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> C C_ f )
132		undif 3882	. . . . . . . . . . . . . 14 |- ( C C_ f <-> ( C u. ( f \ C ) ) = f )
133	131, 132	sylib 199	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( C u. ( f \ C ) ) = f )
134	89, 133	sseq12d 3499	. . . . . . . . . . . 12 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) <-> ( h u. C ) C_ f ) )
135		ssun1 3635	. . . . . . . . . . . . 13 |- h C_ ( h u. C )
136		sstr 3478	. . . . . . . . . . . . 13 |- ( ( h C_ ( h u. C ) /\ ( h u. C ) C_ f ) -> h C_ f )
137	135, 136	mpan 674	. . . . . . . . . . . 12 |- ( ( h u. C ) C_ f -> h C_ f )
138	134, 137	syl6bi 231	. . . . . . . . . . 11 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) -> h C_ f ) )
139	85, 138	syl5 33	. . . . . . . . . 10 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> ( ( h \ C ) C_ ( f \ C ) -> h C_ f ) )
140	84, 139	mpd 15	. . . . . . . . 9 |- ( ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) /\ h e. A ) -> h C_ f )
141	140	ralrimiva 2846	. . . . . . . 8 |- ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> A. h e. A h C_ f )
142		unissb 4253	. . . . . . . 8 |- ( U. A C_ f <-> A. h e. A h C_ f )
143	141, 142	sylibr 215	. . . . . . 7 |- ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> U. A C_ f )
144		elssuni 4251	. . . . . . . 8 |- ( f e. A -> f C_ U. A )
145	144	ad2antrl 732	. . . . . . 7 |- ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> f C_ U. A )
146	143, 145	eqssd 3487	. . . . . 6 |- ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> U. A = f )
147		simprl 762	. . . . . 6 |- ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> f e. A )
148	146, 147	eqeltrd 2517	. . . . 5 |- ( ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) /\ ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) ) -> U. A e. A )
149	148	rexlimdvaa 2925	. . . 4 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> ( E. f e. A U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) -> U. A e. A ) )
150	68, 149	syl5 33	. . 3 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> ( U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) -> U. A e. A ) )
151	64, 150	mtod 180	. 2 |- ( ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) /\ ( B \ C ) e. FinII ) -> -. U. ran ( g e. A |-> ( g \ C ) ) e. ran ( g e. A |-> ( g \ C ) ) )
152	63, 151	pm2.65da 578	1 |- ( ( ( A C_ ~P B /\ [ C.] Or A /\ -. U. A e. A ) /\ ( -. C e. Fin /\ C e. A ) ) -> -. ( B \ C ) e. FinII )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   =/= wne 2625   A.wral 2782   E.wrex 2783   _Vcvv 3087   \ cdif 3439   u. cun 3440   C_ wss 3442   (/)c0 3767   ~Pcpw 3985   U.cuni 4222   |-> cmpt 4484   Or wor 4774   ran crn 4855   [ C.] crpss 6584   Fincfn 7577  Fin^IIcfin2 8707

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 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661

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 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-po 4775  df-so 4776  df-xp 4860  df-rel 4861  df-cnv 4862  df-dm 4864  df-rn 4865  df-rpss 6585  df-fin2 8714

This theorem is referenced by:  fin1a2s  8842