Theorem fin1a2lem13 8868

Description: Lemma for fin1a2 8871. (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 467	. . 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 1053	. . . 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 3439	. . . . . . . . . 10 |- ( ( A C_ ~P B /\ g e. A ) -> g e. ~P B )
4	3	elpwid 3973	. . . . . . . . 9 |- ( ( A C_ ~P B /\ g e. A ) -> g C_ B )
5	4	ssdifd 3581	. . . . . . . 8 |- ( ( A C_ ~P B /\ g e. A ) -> ( g \ C ) C_ ( B \ C ) )
6		sseq1 3465	. . . . . . . 8 |- ( f = ( g \ C ) -> ( f C_ ( B \ C ) <-> ( g \ C ) C_ ( B \ C ) ) )
7	5, 6	syl5ibrcom 230	. . . . . . 7 |- ( ( A C_ ~P B /\ g e. A ) -> ( f = ( g \ C ) -> f C_ ( B \ C ) ) )
8	7	rexlimdva 2891	. . . . . 6 |- ( A C_ ~P B -> ( E. g e. A f = ( g \ C ) -> f C_ ( B \ C ) ) )
9		vex 3060	. . . . . . 7 |- f e. _V
10		eqid 2462	. . . . . . . 8 |- ( g e. A |-> ( g \ C ) ) = ( g e. A |-> ( g \ C ) )
11	10	elrnmpt 5100	. . . . . . 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 3970	. . . . . 6 |- ( f e. ~P ( B \ C ) <-> f C_ ( B \ C ) )
14	8, 12, 13	3imtr4g 278	. . . . 5 |- ( A C_ ~P B -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> f e. ~P ( B \ C ) ) )
15	14	ssrdv 3450	. . . 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 776	. . . 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 3847	. . . . . . 7 |- ( C \ C ) = (/)
19	18	eqcomi 2471	. . . . . 6 |- (/) = ( C \ C )
20		difeq1 3556	. . . . . . . 8 |- ( g = C -> ( g \ C ) = ( C \ C ) )
21	20	eqeq2d 2472	. . . . . . 7 |- ( g = C -> ( (/) = ( g \ C ) <-> (/) = ( C \ C ) ) )
22	21	rspcev 3162	. . . . . 6 |- ( ( C e. A /\ (/) = ( C \ C ) ) -> E. g e. A (/) = ( g \ C ) )
23	19, 22	mpan2 682	. . . . 5 |- ( C e. A -> E. g e. A (/) = ( g \ C ) )
24		0ex 4549	. . . . . 6 |- (/) e. _V
25	10	elrnmpt 5100	. . . . . 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 217	. . . 4 |- ( C e. A -> (/) e. ran ( g e. A |-> ( g \ C ) ) )
28		ne0i 3749	. . . 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 1054	. . . 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 3060	. . . . . . . 8 |- x e. _V
32	10	elrnmpt 5100	. . . . . . . 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 3556	. . . . . . . . . 10 |- ( g = e -> ( g \ C ) = ( e \ C ) )
35	34	eqeq2d 2472	. . . . . . . . 9 |- ( g = e -> ( x = ( g \ C ) <-> x = ( e \ C ) ) )
36	35	cbvrexv 3032	. . . . . . . 8 |- ( E. g e. A x = ( g \ C ) <-> E. e e. A x = ( e \ C ) )
37		sorpssi 6604	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( e C_ g \/ g C_ e ) )
38		ssdif 3580	. . . . . . . . . . . . . . . . 17 |- ( e C_ g -> ( e \ C ) C_ ( g \ C ) )
39		ssdif 3580	. . . . . . . . . . . . . . . . 17 |- ( g C_ e -> ( g \ C ) C_ ( e \ C ) )
40	38, 39	orim12i 523	. . . . . . . . . . . . . . . 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 3466	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( ( e \ C ) C_ f <-> ( e \ C ) C_ ( g \ C ) ) )
43		sseq1 3465	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( f C_ ( e \ C ) <-> ( g \ C ) C_ ( e \ C ) ) )
44	42, 43	orbi12d 721	. . . . . . . . . . . . . . 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 230	. . . . . . . . . . . . . 14 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
46	45	expr 624	. . . . . . . . . . . . 13 |- ( ( [ C.] Or A /\ e e. A ) -> ( g e. A -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) ) )
47	46	rexlimdv 2889	. . . . . . . . . . . 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 225	. . . . . . . . . . 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 2812	. . . . . . . . . 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 3465	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( x C_ f <-> ( e \ C ) C_ f ) )
51		sseq2 3466	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( f C_ x <-> f C_ ( e \ C ) ) )
52	50, 51	orbi12d 721	. . . . . . . . . . 11 |- ( x = ( e \ C ) -> ( ( x C_ f \/ f C_ x ) <-> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
53	52	ralbidv 2839	. . . . . . . . . 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 230	. . . . . . . . 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 2891	. . . . . . . 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 225	. . . . . . 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 225	. . . . . 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 2812	. . . . 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 6603	. . . . 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 217	. . . 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 8751	. . 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 1277	. 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 1055	. . 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 3556	. . . . . . 7 |- ( g = f -> ( g \ C ) = ( f \ C ) )
66	65	cbvmptv 4509	. . . . . 6 |- ( g e. A |-> ( g \ C ) ) = ( f e. A |-> ( f \ C ) )
67	66	elrnmpt 5100	. . . . 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 249	. . . 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 2462	. . . . . . . . . . . . . . . 16 |- ( h \ C ) = ( h \ C )
70		difeq1 3556	. . . . . . . . . . . . . . . . . 18 |- ( g = h -> ( g \ C ) = ( h \ C ) )
71	70	eqeq2d 2472	. . . . . . . . . . . . . . . . 17 |- ( g = h -> ( ( h \ C ) = ( g \ C ) <-> ( h \ C ) = ( h \ C ) ) )
72	71	rspcev 3162	. . . . . . . . . . . . . . . 16 |- ( ( h e. A /\ ( h \ C ) = ( h \ C ) ) -> E. g e. A ( h \ C ) = ( g \ C ) )
73	69, 72	mpan2 682	. . . . . . . . . . . . . . 15 |- ( h e. A -> E. g e. A ( h \ C ) = ( g \ C ) )
74	73	adantl 472	. . . . . . . . . . . . . 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 3060	. . . . . . . . . . . . . . 15 |- h e. _V
76		difexg 4565	. . . . . . . . . . . . . . 15 |- ( h e. _V -> ( h \ C ) e. _V )
77	10	elrnmpt 5100	. . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . 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 4241	. . . . . . . . . . . . 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 767	. . . . . . . . . . . 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 3480	. . . . . . . . . . 11 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
84	83	adantll 725	. . . . . . . . . 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 3617	. . . . . . . . . . 11 |- ( ( h \ C ) C_ ( f \ C ) -> ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) )
86		uncom 3590	. . . . . . . . . . . . . . 15 |- ( C u. ( h \ C ) ) = ( ( h \ C ) u. C )
87		undif1 3854	. . . . . . . . . . . . . . 15 |- ( ( h \ C ) u. C ) = ( h u. C )
88	86, 87	eqtri 2484	. . . . . . . . . . . . . 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 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 ) -> -. U. A e. A )
91	17	ad2antrr 737	. . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . 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 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x \ C ) = ( x \ C )
94		difeq1 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( g = x -> ( g \ C ) = ( x \ C ) )
95	94	eqeq2d 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( g = x -> ( ( x \ C ) = ( g \ C ) <-> ( x \ C ) = ( x \ C ) ) )
96	95	rspcev 3162	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A /\ ( x \ C ) = ( x \ C ) ) -> E. g e. A ( x \ C ) = ( g \ C ) )
97	93, 96	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. A -> E. g e. A ( x \ C ) = ( g \ C ) )
98		difexg 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. _V -> ( x \ C ) e. _V )
99	10	elrnmpt 5100	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. A -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
102	101	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 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 774	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f C_ C <-> ( f \ C ) = (/) )
105	104	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f C_ C -> ( f \ C ) = (/) )
106	105	ad2antlr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2496	. . . . . . . . . . . . . . . . . . . . . . . . 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 4238	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( U. ran ( g e. A |-> ( g \ C ) ) = (/) <-> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
109	107, 108	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . 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 2466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( e = ( x \ C ) -> ( e = (/) <-> ( x \ C ) = (/) ) )
111	110	rspcva 3160	. . . . . . . . . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) = (/) )
113		ssdif0 3835	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x C_ C <-> ( x \ C ) = (/) )
114	112, 113	sylibr 217	. . . . . . . . . . . . . . . . . . . . . 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 2814	. . . . . . . . . . . . . . . . . . . . 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 4243	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. A C_ C <-> A. x e. A x C_ C )
117	115, 116	sylibr 217	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A C_ C )
118		elssuni 4241	. . . . . . . . . . . . . . . . . . . . 21 |- ( C e. A -> C C_ U. A )
119	118	ad2antrr 737	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C C_ U. A )
120	117, 119	eqssd 3461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A = C )
121		simpll 765	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C e. A )
122	120, 121	eqeltrd 2540	. . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A e. A )
123	122	ex 440	. . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . 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 182	. . . . . . . . . . . . . . 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 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 ) -> [ C.] Or A )
127		simplrl 775	. . . . . . . . . . . . . . . 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 6604	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( f e. A /\ C e. A ) ) -> ( f C_ C \/ C C_ f ) )
129	126, 127, 91, 128	syl12anc 1274	. . . . . . . . . . . . . . 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 388	. . . . . . . . . . . . . . 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 3860	. . . . . . . . . . . . . 14 |- ( C C_ f <-> ( C u. ( f \ C ) ) = f )
133	131, 132	sylib 201	. . . . . . . . . . . . 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 3473	. . . . . . . . . . . 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 3609	. . . . . . . . . . . . 13 |- h C_ ( h u. C )
136		sstr 3452	. . . . . . . . . . . . 13 |- ( ( h C_ ( h u. C ) /\ ( h u. C ) C_ f ) -> h C_ f )
137	135, 136	mpan 681	. . . . . . . . . . . 12 |- ( ( h u. C ) C_ f -> h C_ f )
138	134, 137	syl6bi 236	. . . . . . . . . . 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 2814	. . . . . . . 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 4243	. . . . . . . 8 |- ( U. A C_ f <-> A. h e. A h C_ f )
143	141, 142	sylibr 217	. . . . . . 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 4241	. . . . . . . 8 |- ( f e. A -> f C_ U. A )
145	144	ad2antrl 739	. . . . . . 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 3461	. . . . . 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 769	. . . . . 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 2540	. . . . 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 2892	. . . 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 182	. 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 584	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 189   \/ wo 374   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057   \ cdif 3413   u. cun 3414   C_ wss 3416   (/)c0 3743   ~Pcpw 3963   U.cuni 4212   |-> cmpt 4475   Or wor 4773   ran crn 4854   [ C.] crpss 6597   Fincfn 7595  Fin^IIcfin2 8735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864  df-rpss 6598  df-fin2 8742

This theorem is referenced by:  fin1a2s  8870