Theorem fin1a2lem13 8248

Description: Lemma for fin1a2 8251. (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 448	. . 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 996	. . . 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 3303	. . . . . . . . . 10 |- ( ( A C_ ~P B /\ g e. A ) -> g e. ~P B )
4	3	elpwid 3768	. . . . . . . . 9 |- ( ( A C_ ~P B /\ g e. A ) -> g C_ B )
5	4	ssdifd 3443	. . . . . . . 8 |- ( ( A C_ ~P B /\ g e. A ) -> ( g \ C ) C_ ( B \ C ) )
6		sseq1 3329	. . . . . . . 8 |- ( f = ( g \ C ) -> ( f C_ ( B \ C ) <-> ( g \ C ) C_ ( B \ C ) ) )
7	5, 6	syl5ibrcom 214	. . . . . . 7 |- ( ( A C_ ~P B /\ g e. A ) -> ( f = ( g \ C ) -> f C_ ( B \ C ) ) )
8	7	rexlimdva 2790	. . . . . 6 |- ( A C_ ~P B -> ( E. g e. A f = ( g \ C ) -> f C_ ( B \ C ) ) )
9		vex 2919	. . . . . . 7 |- f e. _V
10		eqid 2404	. . . . . . . 8 |- ( g e. A |-> ( g \ C ) ) = ( g e. A |-> ( g \ C ) )
11	10	elrnmpt 5076	. . . . . . 7 |- ( f e. _V -> ( f e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A f = ( g \ C ) ) )
12	9, 11	ax-mp 8	. . . . . 6 |- ( f e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A f = ( g \ C ) )
13	9	elpw 3765	. . . . . 6 |- ( f e. ~P ( B \ C ) <-> f C_ ( B \ C ) )
14	8, 12, 13	3imtr4g 262	. . . . 5 |- ( A C_ ~P B -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> f e. ~P ( B \ C ) ) )
15	14	ssrdv 3314	. . . 4 |- ( A C_ ~P B -> ran ( g e. A |-> ( g \ C ) ) C_ ~P ( B \ C ) )
16	2, 15	syl 16	. . 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 738	. . . 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 3656	. . . . . . 7 |- ( C \ C ) = (/)
19	18	eqcomi 2408	. . . . . 6 |- (/) = ( C \ C )
20		difeq1 3418	. . . . . . . 8 |- ( g = C -> ( g \ C ) = ( C \ C ) )
21	20	eqeq2d 2415	. . . . . . 7 |- ( g = C -> ( (/) = ( g \ C ) <-> (/) = ( C \ C ) ) )
22	21	rspcev 3012	. . . . . 6 |- ( ( C e. A /\ (/) = ( C \ C ) ) -> E. g e. A (/) = ( g \ C ) )
23	19, 22	mpan2 653	. . . . 5 |- ( C e. A -> E. g e. A (/) = ( g \ C ) )
24		0ex 4299	. . . . . 6 |- (/) e. _V
25	10	elrnmpt 5076	. . . . . 6 |- ( (/) e. _V -> ( (/) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A (/) = ( g \ C ) ) )
26	24, 25	ax-mp 8	. . . . 5 |- ( (/) e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A (/) = ( g \ C ) )
27	23, 26	sylibr 204	. . . 4 |- ( C e. A -> (/) e. ran ( g e. A |-> ( g \ C ) ) )
28		ne0i 3594	. . . 4 |- ( (/) e. ran ( g e. A |-> ( g \ C ) ) -> ran ( g e. A |-> ( g \ C ) ) =/= (/) )
29	17, 27, 28	3syl 19	. . 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 997	. . . 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 2919	. . . . . . . 8 |- x e. _V
32	10	elrnmpt 5076	. . . . . . . 8 |- ( x e. _V -> ( x e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A x = ( g \ C ) ) )
33	31, 32	ax-mp 8	. . . . . . 7 |- ( x e. ran ( g e. A |-> ( g \ C ) ) <-> E. g e. A x = ( g \ C ) )
34		difeq1 3418	. . . . . . . . . 10 |- ( g = e -> ( g \ C ) = ( e \ C ) )
35	34	eqeq2d 2415	. . . . . . . . 9 |- ( g = e -> ( x = ( g \ C ) <-> x = ( e \ C ) ) )
36	35	cbvrexv 2893	. . . . . . . 8 |- ( E. g e. A x = ( g \ C ) <-> E. e e. A x = ( e \ C ) )
37		sorpssi 6487	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( e C_ g \/ g C_ e ) )
38		ssdif 3442	. . . . . . . . . . . . . . . . 17 |- ( e C_ g -> ( e \ C ) C_ ( g \ C ) )
39		ssdif 3442	. . . . . . . . . . . . . . . . 17 |- ( g C_ e -> ( g \ C ) C_ ( e \ C ) )
40	38, 39	orim12i 503	. . . . . . . . . . . . . . . 16 |- ( ( e C_ g \/ g C_ e ) -> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) )
41	37, 40	syl 16	. . . . . . . . . . . . . . 15 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( ( e \ C ) C_ ( g \ C ) \/ ( g \ C ) C_ ( e \ C ) ) )
42		sseq2 3330	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( ( e \ C ) C_ f <-> ( e \ C ) C_ ( g \ C ) ) )
43		sseq1 3329	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( f C_ ( e \ C ) <-> ( g \ C ) C_ ( e \ C ) ) )
44	42, 43	orbi12d 691	. . . . . . . . . . . . . . 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 214	. . . . . . . . . . . . . 14 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
46	45	expr 599	. . . . . . . . . . . . 13 |- ( ( [ C.] Or A /\ e e. A ) -> ( g e. A -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) ) )
47	46	rexlimdv 2789	. . . . . . . . . . . 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 209	. . . . . . . . . . 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 2748	. . . . . . . . . 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 3329	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( x C_ f <-> ( e \ C ) C_ f ) )
51		sseq2 3330	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( f C_ x <-> f C_ ( e \ C ) ) )
52	50, 51	orbi12d 691	. . . . . . . . . . 11 |- ( x = ( e \ C ) -> ( ( x C_ f \/ f C_ x ) <-> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
53	52	ralbidv 2686	. . . . . . . . . 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 214	. . . . . . . . 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 2790	. . . . . . . 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 209	. . . . . . 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 209	. . . . . 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 2748	. . . . 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 6486	. . . . 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 204	. . . 4 |- ( [ C.] Or A -> [ C.] Or ran ( g e. A |-> ( g \ C ) ) )
61	30, 60	syl 16	. . 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 8131	. . 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 1185	. 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 998	. . 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 3418	. . . . . . 7 |- ( g = f -> ( g \ C ) = ( f \ C ) )
66	65	cbvmptv 4260	. . . . . 6 |- ( g e. A |-> ( g \ C ) ) = ( f e. A |-> ( f \ C ) )
67	66	elrnmpt 5076	. . . . 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 233	. . . 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 2404	. . . . . . . . . . . . . . . 16 |- ( h \ C ) = ( h \ C )
70		difeq1 3418	. . . . . . . . . . . . . . . . . 18 |- ( g = h -> ( g \ C ) = ( h \ C ) )
71	70	eqeq2d 2415	. . . . . . . . . . . . . . . . 17 |- ( g = h -> ( ( h \ C ) = ( g \ C ) <-> ( h \ C ) = ( h \ C ) ) )
72	71	rspcev 3012	. . . . . . . . . . . . . . . 16 |- ( ( h e. A /\ ( h \ C ) = ( h \ C ) ) -> E. g e. A ( h \ C ) = ( g \ C ) )
73	69, 72	mpan2 653	. . . . . . . . . . . . . . 15 |- ( h e. A -> E. g e. A ( h \ C ) = ( g \ C ) )
74	73	adantl 453	. . . . . . . . . . . . . 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 2919	. . . . . . . . . . . . . . 15 |- h e. _V
76		difexg 4311	. . . . . . . . . . . . . . 15 |- ( h e. _V -> ( h \ C ) e. _V )
77	10	elrnmpt 5076	. . . . . . . . . . . . . . 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 204	. . . . . . . . . . . . 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 4003	. . . . . . . . . . . . 13 |- ( ( h \ C ) e. ran ( g e. A |-> ( g \ C ) ) -> ( h \ C ) C_ U. ran ( g e. A |-> ( g \ C ) ) )
81	79, 80	syl 16	. . . . . . . . . . . 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 732	. . . . . . . . . . . 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 3344	. . . . . . . . . . 11 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
84	83	adantll 695	. . . . . . . . . 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 3478	. . . . . . . . . . 11 |- ( ( h \ C ) C_ ( f \ C ) -> ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) )
86		uncom 3451	. . . . . . . . . . . . . . 15 |- ( C u. ( h \ C ) ) = ( ( h \ C ) u. C )
87		undif1 3663	. . . . . . . . . . . . . . 15 |- ( ( h \ C ) u. C ) = ( h u. C )
88	86, 87	eqtri 2424	. . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . 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 738	. . . . . . . . . . . . . . . . 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 2404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x \ C ) = ( x \ C )
94		difeq1 3418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( g = x -> ( g \ C ) = ( x \ C ) )
95	94	eqeq2d 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( g = x -> ( ( x \ C ) = ( g \ C ) <-> ( x \ C ) = ( x \ C ) ) )
96	95	rspcev 3012	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A /\ ( x \ C ) = ( x \ C ) ) -> E. g e. A ( x \ C ) = ( g \ C ) )
97	93, 96	mpan2 653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. A -> E. g e. A ( x \ C ) = ( g \ C ) )
98		difexg 4311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. _V -> ( x \ C ) e. _V )
99	10	elrnmpt 5076	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 204	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. A -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
102	101	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . 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 736	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3646	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f C_ C <-> ( f \ C ) = (/) )
105	104	biimpi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f C_ C -> ( f \ C ) = (/) )
106	105	ad2antlr 708	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2436	. . . . . . . . . . . . . . . . . . . . . . . . 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 4001	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( U. ran ( g e. A |-> ( g \ C ) ) = (/) <-> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
109	107, 108	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . 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 2410	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( e = ( x \ C ) -> ( e = (/) <-> ( x \ C ) = (/) ) )
111	110	rspcva 3010	. . . . . . . . . . . . . . . . . . . . . . . 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 643	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) = (/) )
113		ssdif0 3646	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x C_ C <-> ( x \ C ) = (/) )
114	112, 113	sylibr 204	. . . . . . . . . . . . . . . . . . . . . 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 2749	. . . . . . . . . . . . . . . . . . . . 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 4005	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. A C_ C <-> A. x e. A x C_ C )
117	115, 116	sylibr 204	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A C_ C )
118		elssuni 4003	. . . . . . . . . . . . . . . . . . . . 21 |- ( C e. A -> C C_ U. A )
119	118	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C C_ U. A )
120	117, 119	eqssd 3325	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A = C )
121		simpll 731	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C e. A )
122	120, 121	eqeltrd 2478	. . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A e. A )
123	122	ex 424	. . . . . . . . . . . . . . . . 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 643	. . . . . . . . . . . . . . . 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 170	. . . . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . 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 737	. . . . . . . . . . . . . . . 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 6487	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( f e. A /\ C e. A ) ) -> ( f C_ C \/ C C_ f ) )
129	126, 127, 91, 128	syl12anc 1182	. . . . . . . . . . . . . . 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 372	. . . . . . . . . . . . . . 15 |- ( -. f C_ C -> ( ( f C_ C \/ C C_ f ) -> C C_ f ) )
131	125, 129, 130	sylc 58	. . . . . . . . . . . . . 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 3668	. . . . . . . . . . . . . 14 |- ( C C_ f <-> ( C u. ( f \ C ) ) = f )
133	131, 132	sylib 189	. . . . . . . . . . . . 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 3337	. . . . . . . . . . . 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 3470	. . . . . . . . . . . . 13 |- h C_ ( h u. C )
136		sstr 3316	. . . . . . . . . . . . 13 |- ( ( h C_ ( h u. C ) /\ ( h u. C ) C_ f ) -> h C_ f )
137	135, 136	mpan 652	. . . . . . . . . . . 12 |- ( ( h u. C ) C_ f -> h C_ f )
138	134, 137	syl6bi 220	. . . . . . . . . . 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 30	. . . . . . . . . 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 2749	. . . . . . . 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 4005	. . . . . . . 8 |- ( U. A C_ f <-> A. h e. A h C_ f )
143	141, 142	sylibr 204	. . . . . . 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 4003	. . . . . . . 8 |- ( f e. A -> f C_ U. A )
145	144	ad2antrl 709	. . . . . . 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 3325	. . . . . 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 733	. . . . . 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 2478	. . . . 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 2791	. . . 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 30	. . 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 170	. 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 560	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 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   \ cdif 3277   u. cun 3278   C_ wss 3280   (/)c0 3588   ~Pcpw 3759   U.cuni 3975   e. cmpt 4226   Or wor 4462   ran crn 4838   [ C.] crpss 6480   Fincfn 7068  Fin^IIcfin2 8115

This theorem is referenced by:  fin1a2s  8250

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-po 4463  df-so 4464  df-xp 4843  df-rel 4844  df-cnv 4845  df-dm 4847  df-rn 4848  df-rpss 6481  df-fin2 8122