Theorem fin1a2lem13 8792

Description: Lemma for fin1a2 8795. (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 461	. . 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 1035	. . . 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 3499	. . . . . . . . . 10 |- ( ( A C_ ~P B /\ g e. A ) -> g e. ~P B )
4	3	elpwid 4020	. . . . . . . . 9 |- ( ( A C_ ~P B /\ g e. A ) -> g C_ B )
5	4	ssdifd 3640	. . . . . . . 8 |- ( ( A C_ ~P B /\ g e. A ) -> ( g \ C ) C_ ( B \ C ) )
6		sseq1 3525	. . . . . . . 8 |- ( f = ( g \ C ) -> ( f C_ ( B \ C ) <-> ( g \ C ) C_ ( B \ C ) ) )
7	5, 6	syl5ibrcom 222	. . . . . . 7 |- ( ( A C_ ~P B /\ g e. A ) -> ( f = ( g \ C ) -> f C_ ( B \ C ) ) )
8	7	rexlimdva 2955	. . . . . 6 |- ( A C_ ~P B -> ( E. g e. A f = ( g \ C ) -> f C_ ( B \ C ) ) )
9		vex 3116	. . . . . . 7 |- f e. _V
10		eqid 2467	. . . . . . . 8 |- ( g e. A |-> ( g \ C ) ) = ( g e. A |-> ( g \ C ) )
11	10	elrnmpt 5249	. . . . . . 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 4017	. . . . . 6 |- ( f e. ~P ( B \ C ) <-> f C_ ( B \ C ) )
14	8, 12, 13	3imtr4g 270	. . . . 5 |- ( A C_ ~P B -> ( f e. ran ( g e. A |-> ( g \ C ) ) -> f e. ~P ( B \ C ) ) )
15	14	ssrdv 3510	. . . 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 760	. . . 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 3895	. . . . . . 7 |- ( C \ C ) = (/)
19	18	eqcomi 2480	. . . . . 6 |- (/) = ( C \ C )
20		difeq1 3615	. . . . . . . 8 |- ( g = C -> ( g \ C ) = ( C \ C ) )
21	20	eqeq2d 2481	. . . . . . 7 |- ( g = C -> ( (/) = ( g \ C ) <-> (/) = ( C \ C ) ) )
22	21	rspcev 3214	. . . . . 6 |- ( ( C e. A /\ (/) = ( C \ C ) ) -> E. g e. A (/) = ( g \ C ) )
23	19, 22	mpan2 671	. . . . 5 |- ( C e. A -> E. g e. A (/) = ( g \ C ) )
24		0ex 4577	. . . . . 6 |- (/) e. _V
25	10	elrnmpt 5249	. . . . . 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 212	. . . 4 |- ( C e. A -> (/) e. ran ( g e. A |-> ( g \ C ) ) )
28		ne0i 3791	. . . 4 |- ( (/) e. ran ( g e. A |-> ( g \ C ) ) -> ran ( g e. A |-> ( g \ C ) ) =/= (/) )
29	17, 27, 28	3syl 20	. . 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 1036	. . . 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 3116	. . . . . . . 8 |- x e. _V
32	10	elrnmpt 5249	. . . . . . . 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 3615	. . . . . . . . . 10 |- ( g = e -> ( g \ C ) = ( e \ C ) )
35	34	eqeq2d 2481	. . . . . . . . 9 |- ( g = e -> ( x = ( g \ C ) <-> x = ( e \ C ) ) )
36	35	cbvrexv 3089	. . . . . . . 8 |- ( E. g e. A x = ( g \ C ) <-> E. e e. A x = ( e \ C ) )
37		sorpssi 6570	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( e C_ g \/ g C_ e ) )
38		ssdif 3639	. . . . . . . . . . . . . . . . 17 |- ( e C_ g -> ( e \ C ) C_ ( g \ C ) )
39		ssdif 3639	. . . . . . . . . . . . . . . . 17 |- ( g C_ e -> ( g \ C ) C_ ( e \ C ) )
40	38, 39	orim12i 516	. . . . . . . . . . . . . . . 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 3526	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( ( e \ C ) C_ f <-> ( e \ C ) C_ ( g \ C ) ) )
43		sseq1 3525	. . . . . . . . . . . . . . . 16 |- ( f = ( g \ C ) -> ( f C_ ( e \ C ) <-> ( g \ C ) C_ ( e \ C ) ) )
44	42, 43	orbi12d 709	. . . . . . . . . . . . . . 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 222	. . . . . . . . . . . . . 14 |- ( ( [ C.] Or A /\ ( e e. A /\ g e. A ) ) -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
46	45	expr 615	. . . . . . . . . . . . 13 |- ( ( [ C.] Or A /\ e e. A ) -> ( g e. A -> ( f = ( g \ C ) -> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) ) )
47	46	rexlimdv 2953	. . . . . . . . . . . 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 217	. . . . . . . . . . 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 2876	. . . . . . . . . 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 3525	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( x C_ f <-> ( e \ C ) C_ f ) )
51		sseq2 3526	. . . . . . . . . . . 12 |- ( x = ( e \ C ) -> ( f C_ x <-> f C_ ( e \ C ) ) )
52	50, 51	orbi12d 709	. . . . . . . . . . 11 |- ( x = ( e \ C ) -> ( ( x C_ f \/ f C_ x ) <-> ( ( e \ C ) C_ f \/ f C_ ( e \ C ) ) ) )
53	52	ralbidv 2903	. . . . . . . . . 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 222	. . . . . . . . 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 2955	. . . . . . . 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 217	. . . . . . 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 217	. . . . . 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 2876	. . . . 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 6569	. . . . 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 212	. . . 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 8675	. . 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 1229	. 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 1037	. . 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 3615	. . . . . . 7 |- ( g = f -> ( g \ C ) = ( f \ C ) )
66	65	cbvmptv 4538	. . . . . 6 |- ( g e. A |-> ( g \ C ) ) = ( f e. A |-> ( f \ C ) )
67	66	elrnmpt 5249	. . . . 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 241	. . . 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 2467	. . . . . . . . . . . . . . . 16 |- ( h \ C ) = ( h \ C )
70		difeq1 3615	. . . . . . . . . . . . . . . . . 18 |- ( g = h -> ( g \ C ) = ( h \ C ) )
71	70	eqeq2d 2481	. . . . . . . . . . . . . . . . 17 |- ( g = h -> ( ( h \ C ) = ( g \ C ) <-> ( h \ C ) = ( h \ C ) ) )
72	71	rspcev 3214	. . . . . . . . . . . . . . . 16 |- ( ( h e. A /\ ( h \ C ) = ( h \ C ) ) -> E. g e. A ( h \ C ) = ( g \ C ) )
73	69, 72	mpan2 671	. . . . . . . . . . . . . . 15 |- ( h e. A -> E. g e. A ( h \ C ) = ( g \ C ) )
74	73	adantl 466	. . . . . . . . . . . . . 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 3116	. . . . . . . . . . . . . . 15 |- h e. _V
76		difexg 4595	. . . . . . . . . . . . . . 15 |- ( h e. _V -> ( h \ C ) e. _V )
77	10	elrnmpt 5249	. . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . 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 4275	. . . . . . . . . . . . 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 754	. . . . . . . . . . . 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 3540	. . . . . . . . . . 11 |- ( ( ( f e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ h e. A ) -> ( h \ C ) C_ ( f \ C ) )
84	83	adantll 713	. . . . . . . . . 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 3675	. . . . . . . . . . 11 |- ( ( h \ C ) C_ ( f \ C ) -> ( C u. ( h \ C ) ) C_ ( C u. ( f \ C ) ) )
86		uncom 3648	. . . . . . . . . . . . . . 15 |- ( C u. ( h \ C ) ) = ( ( h \ C ) u. C )
87		undif1 3902	. . . . . . . . . . . . . . 15 |- ( ( h \ C ) u. C ) = ( h u. C )
88	86, 87	eqtri 2496	. . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . 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 760	. . . . . . . . . . . . . . . . 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 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x \ C ) = ( x \ C )
94		difeq1 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( g = x -> ( g \ C ) = ( x \ C ) )
95	94	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( g = x -> ( ( x \ C ) = ( g \ C ) <-> ( x \ C ) = ( x \ C ) ) )
96	95	rspcev 3214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. A /\ ( x \ C ) = ( x \ C ) ) -> E. g e. A ( x \ C ) = ( g \ C ) )
97	93, 96	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. A -> E. g e. A ( x \ C ) = ( g \ C ) )
98		difexg 4595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. _V -> ( x \ C ) e. _V )
99	10	elrnmpt 5249	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. A -> ( x \ C ) e. ran ( g e. A |-> ( g \ C ) ) )
102	101	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 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 758	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( f C_ C <-> ( f \ C ) = (/) )
105	104	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( f C_ C -> ( f \ C ) = (/) )
106	105	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2508	. . . . . . . . . . . . . . . . . . . . . . . . 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 4271	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( U. ran ( g e. A |-> ( g \ C ) ) = (/) <-> A. e e. ran ( g e. A |-> ( g \ C ) ) e = (/) )
109	107, 108	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 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 2471	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( e = ( x \ C ) -> ( e = (/) <-> ( x \ C ) = (/) ) )
111	110	rspcva 3212	. . . . . . . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) /\ x e. A ) -> ( x \ C ) = (/) )
113		ssdif0 3885	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x C_ C <-> ( x \ C ) = (/) )
114	112, 113	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 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 2878	. . . . . . . . . . . . . . . . . . . . 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 4277	. . . . . . . . . . . . . . . . . . . . 21 |- ( U. A C_ C <-> A. x e. A x C_ C )
117	115, 116	sylibr 212	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A C_ C )
118		elssuni 4275	. . . . . . . . . . . . . . . . . . . . 21 |- ( C e. A -> C C_ U. A )
119	118	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C C_ U. A )
120	117, 119	eqssd 3521	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A = C )
121		simpll 753	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> C e. A )
122	120, 121	eqeltrd 2555	. . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. A /\ U. ran ( g e. A |-> ( g \ C ) ) = ( f \ C ) ) /\ f C_ C ) -> U. A e. A )
123	122	ex 434	. . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . 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 177	. . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . 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 759	. . . . . . . . . . . . . . . 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 6570	. . . . . . . . . . . . . . . 16 |- ( ( [ C.] Or A /\ ( f e. A /\ C e. A ) ) -> ( f C_ C \/ C C_ f ) )
129	126, 127, 91, 128	syl12anc 1226	. . . . . . . . . . . . . . 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 382	. . . . . . . . . . . . . . 15 |- ( -. f C_ C -> ( ( f C_ C \/ C C_ f ) -> C C_ f ) )
131	125, 129, 130	sylc 60	. . . . . . . . . . . . . 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 3907	. . . . . . . . . . . . . 14 |- ( C C_ f <-> ( C u. ( f \ C ) ) = f )
133	131, 132	sylib 196	. . . . . . . . . . . . 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 3533	. . . . . . . . . . . 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 3667	. . . . . . . . . . . . 13 |- h C_ ( h u. C )
136		sstr 3512	. . . . . . . . . . . . 13 |- ( ( h C_ ( h u. C ) /\ ( h u. C ) C_ f ) -> h C_ f )
137	135, 136	mpan 670	. . . . . . . . . . . 12 |- ( ( h u. C ) C_ f -> h C_ f )
138	134, 137	syl6bi 228	. . . . . . . . . . 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 32	. . . . . . . . . 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 2878	. . . . . . . 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 4277	. . . . . . . 8 |- ( U. A C_ f <-> A. h e. A h C_ f )
143	141, 142	sylibr 212	. . . . . . 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 4275	. . . . . . . 8 |- ( f e. A -> f C_ U. A )
145	144	ad2antrl 727	. . . . . . 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 3521	. . . . . 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 755	. . . . . 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 2555	. . . . 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 2956	. . . 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 32	. . 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 177	. 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 576	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 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   \ cdif 3473   u. cun 3474   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   U.cuni 4245   |-> cmpt 4505   Or wor 4799   ran crn 5000   [ C.] crpss 6563   Fincfn 7516  Fin^IIcfin2 8659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-po 4800  df-so 4801  df-xp 5005  df-rel 5006  df-cnv 5007  df-dm 5009  df-rn 5010  df-rpss 6564  df-fin2 8666

This theorem is referenced by:  fin1a2s  8794