Theorem fin1a2lem13 9234

Description: Lemma for fin1a2 9237. (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 477	. . 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 1100	. . . 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 3598	. . . . . . . . . 10 |- ( ( A C_ ~P B /\ g e. A ) -> g e. ~P B )
4	3	elpwid 4170	. . . . . . . . 9 |- ( ( A C_ ~P B /\ g e. A ) -> g C_ B )
5	4	ssdifd 3746	. . . . . . . 8 |- ( ( A C_ ~P B /\ g e. A ) -> ( g \ C ) C_ ( B \ C ) )
6		sseq1 3626	. . . . . . . 8 |- ( f = ( g \ C ) -> ( f C_ ( B \ C ) <-> ( g \ C ) C_ ( B \ C ) ) )
7	5, 6	syl5ibrcom 237	. . . . . . 7 |- ( ( A C_ ~P B /\ g e. A ) -> ( f = ( g \ C ) -> f C_ ( B \ C ) ) )
8	7	rexlimdva 3031	. . . . . 6 |- ( A C_ ~P B -> ( E. g e. A f = ( g \ C ) -> f C_ ( B \ C ) ) )
9		vex 3203	. . . . . . 7 |- f e. _V
10		eqid 2622	. . . . . . . 8 |- ( g e. A |-> ( g \ C ) ) = ( g e. A |-> ( g \ C ) )
11	10	elrnmpt 5372	. . . . . . 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 4165	. . . . . 6 |- ( f e. ~P ( B \ C ) <-> f C_ ( B \ C ) )
14	8, 12, 13	3imtr4g 285	. . . . 5 |- ( A C_ ~P B -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> f e. ~P ( B \ C ) ) )
15	14	ssrdv 3609	. . . 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 801	. . . 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 3948	. . . . . . 7 |- ( C \ C ) = (/)
19	18	eqcomi 2631	. . . . . 6 |- (/) = ( C \ C )
20		difeq1 3721	. . . . . . . 8 |- ( g = C -> ( g \ C ) = ( C \ C ) )
21	20	eqeq2d 2632	. . . . . . 7 |- ( g = C -> ( (/) = ( g \ C ) <-> (/) = ( C \ C ) ) )
22	21	rspcev 3309	. . . . . 6 |- ( ( C e. A /\ (/) = ( C \ C ) ) -> E. g e. A (/) = ( g \ C ) )
23	19, 22	mpan2 707	. . . . 5 |- ( C e. A -> E. g e. A (/) = ( g \ C ) )
24		0ex 4790	. . . . . 6 |- (/) e. _V
25	10	elrnmpt 5372	. . . . . 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 224	. . . 4 |- ( C e. A -> (/) e. ran ( g e. A |-> ( g \ C ) ) )
28		ne0i 3921	. . . 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 1101	. . . 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 3203	. . . . . . . 8 |- x e. _V
32	10	elrnmpt 5372	. . . . . . . 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 3721	. . . . . . . . . 10 |- ( g = e -> ( g \ C ) = ( e \ C ) )
35	34	eqeq2d 2632	. . . . . . . . 9 |- ( g = e -> ( x = ( g \ C ) <-> x = ( e \ C ) ) )
36	35	cbvrexv 3172	. . . . . . . 8 |- ( E. g e. A x = ( g \ C ) <-> E. e e. A x = ( e \ C ) )
37		sorpssi 6943	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( e C_ g \/ g C_ e ) )
38		ssdif 3745	. . . . . . . . . . . . . . . . 17 |- ( e C_ g -> ( e \ C ) C_ ( g \ C ) )
39		ssdif 3745	. . . . . . . . . . . . . . . . 17 |- ( g C_ e -> ( g \ C ) C_ ( e \ C ) )
40	38, 39	orim12i 538	. . . . . . . . . . . . . . . 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 3627	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( ( e \ C ) C_ f <-> ( e \ C ) C_ ( g \ C ) ) )
43		sseq1 3626	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( f C_ ( e \ C ) <-> ( g \ C ) C_ ( e \ C ) ) )
44	42, 43	orbi12d 746	. . . . . . . . . . . . . . 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 237	. . . . . . . . . . . . . 14 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
46	45	expr 643	. . . . . . . . . . . . 13 |- ( ( [ C.] Or A /\ e e. A ) -> ( g e. A -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) ) )
47	46	rexlimdv 3030	. . . . . . . . . . . 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 232	. . . . . . . . . . 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 2965	. . . . . . . . . 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 3626	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( x C_ f <-> ( e \ C ) C_ f ) )
51		sseq2 3627	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( f C_ x <-> f C_ ( e \ C ) ) )
52	50, 51	orbi12d 746	. . . . . . . . . . 11 |- ( x = ( e \ C ) -> ( ( x C_ f \/ f C_ x ) <-> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
53	52	ralbidv 2986	. . . . . . . . . 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 237	. . . . . . . . 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 3031	. . . . . . . 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 232	. . . . . . 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 232	. . . . . 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 2965	. . . . 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 6942	. . . . 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 224	. . . 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 9117	. . 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 1327	. 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 1102	. . 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 3721	. . . . . . 7 |- ( g = f -> ( g \ C ) = ( f \ C ) )
66	65	cbvmptv 4750	. . . . . 6 |- ( g e. A |-> ( g \ C ) ) = ( f e. A |-> ( f \ C ) )
67	66	elrnmpt 5372	. . . . 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 256	. . . 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 2622	. . . . . . . . . . . . . . . 16 |- ( h \ C ) = ( h \ C )
70		difeq1 3721	. . . . . . . . . . . . . . . . . 18 |- ( g = h -> ( g \ C ) = ( h \ C ) )
71	70	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 |- ( g = h -> ( ( h \ C ) = ( g \ C ) <-> ( h \ C ) = ( h \ C ) ) )
72	71	rspcev 3309	. . . . . . . . . . . . . . . 16 |- ( ( h e. A /\ ( h \ C ) = ( h \ C ) ) -> E. g e. A ( h \ C ) = ( g \ C ) )
73	69, 72	mpan2 707	. . . . . . . . . . . . . . 15 |- ( h e. A -> E. g e. A ( h \ C ) = ( g \ C ) )
74	73	adantl 482	. . . . . . . . . . . . . 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 3203	. . . . . . . . . . . . . . 15 |- h e. _V
76		difexg 4808	. . . . . . . . . . . . . . 15 |- ( h e. _V -> ( h \ C ) e. _V )
77	10	elrnmpt 5372	. . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . 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 4467	. . . . . . . . . . . . 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 792	. . . . . . . . . . . 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 3641	. . . . . . . . . . 11 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
84	83	adantll 750	. . . . . . . . . 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 3784	. . . . . . . . . . 11 |- ( ( h \ C ) C_ ( f \ C ) -> ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) )
86		uncom 3757	. . . . . . . . . . . . . . 15 |- ( C u. ( h \ C ) ) = ( ( h \ C ) u. C )
87		undif1 4043	. . . . . . . . . . . . . . 15 |- ( ( h \ C ) u. C ) = ( h u. C )
88	86, 87	eqtri 2644	. . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . . 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 801	. . . . . . . . . . . . . . . . 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 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x \ C ) = ( x \ C )
94		difeq1 3721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( g = x -> ( g \ C ) = ( x \ C ) )
95	94	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( g = x -> ( ( x \ C ) = ( g \ C ) <-> ( x \ C ) = ( x \ C ) ) )
96	95	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A /\ ( x \ C ) = ( x \ C ) ) -> E. g e. A ( x \ C ) = ( g \ C ) )
97	93, 96	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. A -> E. g e. A ( x \ C ) = ( g \ C ) )
98		difexg 4808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. _V -> ( x \ C ) e. _V )
99	10	elrnmpt 5372	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. A -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
102	101	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 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 799	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f C_ C <-> ( f \ C ) = (/) )
105	104	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f C_ C -> ( f \ C ) = (/) )
106	105	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2656	. . . . . . . . . . . . . . . . . . . . . . . . 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 4464	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( U. ran ( g e. A |-> ( g \ C ) ) = (/) <-> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
109	107, 108	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 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 2626	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( e = ( x \ C ) -> ( e = (/) <-> ( x \ C ) = (/) ) )
111	110	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) = (/) )
113		ssdif0 3942	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x C_ C <-> ( x \ C ) = (/) )
114	112, 113	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 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 2966	. . . . . . . . . . . . . . . . . . . . 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 4469	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. A C_ C <-> A. x e. A x C_ C )
117	115, 116	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A C_ C )
118		elssuni 4467	. . . . . . . . . . . . . . . . . . . . 21 |- ( C e. A -> C C_ U. A )
119	118	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C C_ U. A )
120	117, 119	eqssd 3620	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A = C )
121		simpll 790	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C e. A )
122	120, 121	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A e. A )
123	122	ex 450	. . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . . 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 189	. . . . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . 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 800	. . . . . . . . . . . . . . . 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 6943	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( f e. A /\ C e. A ) ) -> ( f C_ C \/ C C_ f ) )
129	126, 127, 91, 128	syl12anc 1324	. . . . . . . . . . . . . . 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 397	. . . . . . . . . . . . . . 15 |- ( -. f C_ C -> ( ( f C_ C \/ C C_ f ) -> C C_ f ) )
131	125, 129, 130	sylc 65	. . . . . . . . . . . . . 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 4049	. . . . . . . . . . . . . 14 |- ( C C_ f <-> ( C u. ( f \ C ) ) = f )
133	131, 132	sylib 208	. . . . . . . . . . . . 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 3634	. . . . . . . . . . . 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 3776	. . . . . . . . . . . . 13 |- h C_ ( h u. C )
136		sstr 3611	. . . . . . . . . . . . 13 |- ( ( h C_ ( h u. C ) /\ ( h u. C ) C_ f ) -> h C_ f )
137	135, 136	mpan 706	. . . . . . . . . . . 12 |- ( ( h u. C ) C_ f -> h C_ f )
138	134, 137	syl6bi 243	. . . . . . . . . . 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 34	. . . . . . . . . 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 2966	. . . . . . . 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 4469	. . . . . . . 8 |- ( U. A C_ f <-> A. h e. A h C_ f )
143	141, 142	sylibr 224	. . . . . . 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 4467	. . . . . . . 8 |- ( f e. A -> f C_ U. A )
145	144	ad2antrl 764	. . . . . . 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 3620	. . . . . 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 794	. . . . . 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 2701	. . . . 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 3032	. . . 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 34	. . 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 189	. 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 600	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 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |-> cmpt 4729   Or wor 5034   ran crn 5115   [ C.] crpss 6936   Fincfn 7955  Fin^IIcfin2 9101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-rpss 6937  df-fin2 9108

This theorem is referenced by:  fin1a2s  9236