Theorem alexsubALTlem4 21854

Description: Lemma for alexsubALT 21855. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)

Hypothesis

Ref	Expression
alexsubALT.1	|- X = U. J

Assertion

Ref	Expression
alexsubALTlem4	|- ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )

Distinct variable groups:   a, b, c, d, x, J   X, a, b, c, d, x

Proof of Theorem alexsubALTlem4

Dummy variables n s t u v w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ralnex 2992	. . . . 5 |- ( A. b e. ( ~P a i^i Fin ) -. X = U. b <-> -. E. b e. ( ~P a i^i Fin ) X = U. b )
2		alexsubALT.1	. . . . . . . 8 |- X = U. J
3	2	alexsubALTlem2 21852	. . . . . . 7 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> E. u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v )
4		elun 3753	. . . . . . . . . 10 |- ( u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) <-> ( u e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } \/ u e. { (/) } ) )
5		sseq2 3627	. . . . . . . . . . . . 13 |- ( z = u -> ( a C_ z <-> a C_ u ) )
6		pweq 4161	. . . . . . . . . . . . . . 15 |- ( z = u -> ~P z = ~P u )
7	6	ineq1d 3813	. . . . . . . . . . . . . 14 |- ( z = u -> ( ~P z i^i Fin ) = ( ~P u i^i Fin ) )
8	7	raleqdv 3144	. . . . . . . . . . . . 13 |- ( z = u -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> A. b e. ( ~P u i^i Fin ) -. X = U. b ) )
9	5, 8	anbi12d 747	. . . . . . . . . . . 12 |- ( z = u -> ( ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) <-> ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) )
10	9	elrab 3363	. . . . . . . . . . 11 |- ( u e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } <-> ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) )
11		velsn 4193	. . . . . . . . . . 11 |- ( u e. { (/) } <-> u = (/) )
12	10, 11	orbi12i 543	. . . . . . . . . 10 |- ( ( u e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } \/ u e. { (/) } ) <-> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) \/ u = (/) ) )
13	4, 12	bitri 264	. . . . . . . . 9 |- ( u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) <-> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) \/ u = (/) ) )
14		ralnex 2992	. . . . . . . . . . . . 13 |- ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v <-> -. E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
15		simprrl 804	. . . . . . . . . . . . . . . . 17 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> a C_ u )
16	15	unissd 4462	. . . . . . . . . . . . . . . 16 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> U. a C_ U. u )
17		sseq1 3626	. . . . . . . . . . . . . . . 16 |- ( X = U. a -> ( X C_ U. u <-> U. a C_ U. u ) )
18	16, 17	syl5ibrcom 237	. . . . . . . . . . . . . . 15 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X = U. a -> X C_ U. u ) )
19		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x i^i u ) C_ x
20		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- x e. _V
21	20	elpw2 4828	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( x i^i u ) e. ~P x <-> ( x i^i u ) C_ x )
22	19, 21	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x i^i u ) e. ~P x
23		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( c = ( x i^i u ) -> U. c = U. ( x i^i u ) )
24	23	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( c = ( x i^i u ) -> ( X = U. c <-> X = U. ( x i^i u ) ) )
25		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( c = ( x i^i u ) -> ~P c = ~P ( x i^i u ) )
26	25	ineq1d 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( c = ( x i^i u ) -> ( ~P c i^i Fin ) = ( ~P ( x i^i u ) i^i Fin ) )
27	26	rexeqdv 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( c = ( x i^i u ) -> ( E. d e. ( ~P c i^i Fin ) X = U. d <-> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) )
28	24, 27	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( c = ( x i^i u ) -> ( ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) <-> ( X = U. ( x i^i u ) -> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) ) )
29	28	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( ( x i^i u ) e. ~P x -> ( X = U. ( x i^i u ) -> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) ) )
30	22, 29	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d ) )
31		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x i^i u ) C_ u
32		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( d C_ ( x i^i u ) /\ ( x i^i u ) C_ u ) -> d C_ u )
33	31, 32	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( d C_ ( x i^i u ) -> d C_ u )
34	33	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( d C_ ( x i^i u ) /\ d e. Fin ) -> ( d C_ u /\ d e. Fin ) )
35		elfpw 8268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( d e. ( ~P ( x i^i u ) i^i Fin ) <-> ( d C_ ( x i^i u ) /\ d e. Fin ) )
36		elfpw 8268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( d e. ( ~P u i^i Fin ) <-> ( d C_ u /\ d e. Fin ) )
37	34, 35, 36	3imtr4i 281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( d e. ( ~P ( x i^i u ) i^i Fin ) -> d e. ( ~P u i^i Fin ) )
38	37	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( d e. ( ~P ( x i^i u ) i^i Fin ) /\ X = U. d ) -> ( d e. ( ~P u i^i Fin ) /\ X = U. d ) )
39	38	reximi2 3010	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( E. d e. ( ~P ( x i^i u ) i^i Fin ) X = U. d -> E. d e. ( ~P u i^i Fin ) X = U. d )
40	30, 39	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> E. d e. ( ~P u i^i Fin ) X = U. d ) )
41		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( d = b -> U. d = U. b )
42	41	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( d = b -> ( X = U. d <-> X = U. b ) )
43	42	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( E. d e. ( ~P u i^i Fin ) X = U. d <-> E. b e. ( ~P u i^i Fin ) X = U. b )
44	40, 43	syl6ib 241	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> E. b e. ( ~P u i^i Fin ) X = U. b ) )
45		dfrex2 2996	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( E. b e. ( ~P u i^i Fin ) X = U. b <-> -. A. b e. ( ~P u i^i Fin ) -. X = U. b )
46	44, 45	syl6ib 241	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( X = U. ( x i^i u ) -> -. A. b e. ( ~P u i^i Fin ) -. X = U. b ) )
47	46	con2d 129	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) )
48	47	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 |- ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) ) )
49	48	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) ) )
50	49	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ u e. ~P ( fi ` x ) ) -> ( a C_ u -> ( A. b e. ( ~P u i^i Fin ) -. X = U. b -> -. X = U. ( x i^i u ) ) ) )
51	50	impd 447	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ u e. ~P ( fi ` x ) ) -> ( ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) -> -. X = U. ( x i^i u ) ) )
52	51	impr 649	. . . . . . . . . . . . . . . . 17 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> -. X = U. ( x i^i u ) )
53	19	unissi 4461	. . . . . . . . . . . . . . . . . . 19 |- U. ( x i^i u ) C_ U. x
54		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( J = ( topGen ` ( fi ` x ) ) -> U. J = U. ( topGen ` ( fi ` x ) ) )
55		fiuni 8334	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. _V -> U. x = U. ( fi ` x ) )
56	20, 55	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U. x = U. ( fi ` x )
57		fibas 20781	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( fi ` x ) e. TopBases
58		unitg 20771	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( fi ` x ) e. TopBases -> U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x ) )
59	57, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U. ( topGen ` ( fi ` x ) ) = U. ( fi ` x )
60	56, 59	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . 23 |- U. x = U. ( topGen ` ( fi ` x ) )
61	54, 60	syl6reqr 2675	. . . . . . . . . . . . . . . . . . . . . 22 |- ( J = ( topGen ` ( fi ` x ) ) -> U. x = U. J )
62	61, 2	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . 21 |- ( J = ( topGen ` ( fi ` x ) ) -> U. x = X )
63	62	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> U. x = X )
64	63	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> U. x = X )
65	53, 64	syl5sseq 3653	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> U. ( x i^i u ) C_ X )
66		eqcom 2629	. . . . . . . . . . . . . . . . . . 19 |- ( X = U. ( x i^i u ) <-> U. ( x i^i u ) = X )
67		eqss 3618	. . . . . . . . . . . . . . . . . . . 20 |- ( U. ( x i^i u ) = X <-> ( U. ( x i^i u ) C_ X /\ X C_ U. ( x i^i u ) ) )
68	67	baib 944	. . . . . . . . . . . . . . . . . . 19 |- ( U. ( x i^i u ) C_ X -> ( U. ( x i^i u ) = X <-> X C_ U. ( x i^i u ) ) )
69	66, 68	syl5bb 272	. . . . . . . . . . . . . . . . . 18 |- ( U. ( x i^i u ) C_ X -> ( X = U. ( x i^i u ) <-> X C_ U. ( x i^i u ) ) )
70	65, 69	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X = U. ( x i^i u ) <-> X C_ U. ( x i^i u ) ) )
71	52, 70	mtbid 314	. . . . . . . . . . . . . . . 16 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> -. X C_ U. ( x i^i u ) )
72		sstr2 3610	. . . . . . . . . . . . . . . . 17 |- ( X C_ U. u -> ( U. u C_ U. ( x i^i u ) -> X C_ U. ( x i^i u ) ) )
73	72	con3rr3 151	. . . . . . . . . . . . . . . 16 |- ( -. X C_ U. ( x i^i u ) -> ( X C_ U. u -> -. U. u C_ U. ( x i^i u ) ) )
74	71, 73	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X C_ U. u -> -. U. u C_ U. ( x i^i u ) ) )
75		nss 3663	. . . . . . . . . . . . . . . . 17 |- ( -. U. u C_ U. ( x i^i u ) <-> E. y ( y e. U. u /\ -. y e. U. ( x i^i u ) ) )
76		df-rex 2918	. . . . . . . . . . . . . . . . 17 |- ( E. y e. U. u -. y e. U. ( x i^i u ) <-> E. y ( y e. U. u /\ -. y e. U. ( x i^i u ) ) )
77	75, 76	bitr4i 267	. . . . . . . . . . . . . . . 16 |- ( -. U. u C_ U. ( x i^i u ) <-> E. y e. U. u -. y e. U. ( x i^i u ) )
78		eluni2 4440	. . . . . . . . . . . . . . . . . 18 |- ( y e. U. u <-> E. w e. u y e. w )
79		elpwi 4168	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( u e. ~P ( fi ` x ) -> u C_ ( fi ` x ) )
80	79	sseld 3602	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u e. ~P ( fi ` x ) -> ( w e. u -> w e. ( fi ` x ) ) )
81	80	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> w e. ( fi ` x ) ) )
82		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22 |- w e. _V
83		elfi 8319	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( w e. _V /\ x e. _V ) -> ( w e. ( fi ` x ) <-> E. t e. ( ~P x i^i Fin ) w = |^| t ) )
84	82, 20, 83	mp2an 708	. . . . . . . . . . . . . . . . . . . . 21 |- ( w e. ( fi ` x ) <-> E. t e. ( ~P x i^i Fin ) w = |^| t )
85	81, 84	syl6ib 241	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> E. t e. ( ~P x i^i Fin ) w = |^| t ) )
86	2	alexsubALTlem3 21853	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) -> E. s e. t A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n )
87	79	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> u C_ ( fi ` x ) )
88	87	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> u C_ ( fi ` x ) )
89		ssfii 8325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. _V -> x C_ ( fi ` x ) )
90	20, 89	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- x C_ ( fi ` x )
91		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ~P x i^i Fin ) C_ ~P x
92	91	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( t e. ( ~P x i^i Fin ) -> t e. ~P x )
93	92	elpwid 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( t e. ( ~P x i^i Fin ) -> t C_ x )
94	93	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) -> t C_ x )
95	94	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> t C_ x )
96		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> s e. t )
97	95, 96	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> s e. x )
98	90, 97	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> s e. ( fi ` x ) )
99	98	snssd 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> { s } C_ ( fi ` x ) )
100	88, 99	unssd 3789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) C_ ( fi ` x ) )
101		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( fi ` x ) e. _V
102	101	elpw2 4828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( u u. { s } ) e. ~P ( fi ` x ) <-> ( u u. { s } ) C_ ( fi ` x ) )
103	100, 102	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) e. ~P ( fi ` x ) )
104		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> a C_ u )
105	104	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> a C_ u )
106		ssun1 3776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- u C_ ( u u. { s } )
107	105, 106	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> a C_ ( u u. { s } ) )
108		unieq 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( n = b -> U. n = U. b )
109	108	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( n = b -> ( X = U. n <-> X = U. b ) )
110	109	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n = b -> ( -. X = U. n <-> -. X = U. b ) )
111	110	cbvralv 3171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n <-> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b )
112	111	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n -> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b )
113	112	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b )
114	103, 107, 113	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( ( u u. { s } ) e. ~P ( fi ` x ) /\ ( a C_ ( u u. { s } ) /\ A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) ) )
115		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( z = ( u u. { s } ) -> ( a C_ z <-> a C_ ( u u. { s } ) ) )
116		pweq 4161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z = ( u u. { s } ) -> ~P z = ~P ( u u. { s } ) )
117	116	ineq1d 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z = ( u u. { s } ) -> ( ~P z i^i Fin ) = ( ~P ( u u. { s } ) i^i Fin ) )
118	117	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( z = ( u u. { s } ) -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) )
119	115, 118	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( z = ( u u. { s } ) -> ( ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) <-> ( a C_ ( u u. { s } ) /\ A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) ) )
120	119	elrab 3363	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( u u. { s } ) e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } <-> ( ( u u. { s } ) e. ~P ( fi ` x ) /\ ( a C_ ( u u. { s } ) /\ A. b e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. b ) ) )
121	114, 120	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } )
122		elun1 3780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( u u. { s } ) e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } -> ( u u. { s } ) e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) )
123	121, 122	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u u. { s } ) e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) )
124		vsnid 4209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- s e. { s }
125		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( s e. { s } -> s e. ( u u. { s } ) )
126	124, 125	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- s e. ( u u. { s } )
127		intss1 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( s e. t -> |^| t C_ s )
128		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( w = |^| t -> ( w C_ s <-> |^| t C_ s ) )
129	127, 128	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( s e. t -> ( w = |^| t -> w C_ s ) )
130	129	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( w = |^| t /\ s e. t ) -> w C_ s )
131	130	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ s e. t ) -> w C_ s )
132	131	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ s e. t ) -> w C_ s )
133	132	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( w e. u /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ s e. t ) ) -> w C_ s )
134	133	adantrrr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( w e. u /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> w C_ s )
135	134	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> w C_ s )
136		simprlr 803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> y e. w )
137	135, 136	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> y e. s )
138	93	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) -> t C_ x )
139	138	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> t C_ x )
140		simprrl 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> s e. t )
141	139, 140	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> s e. x )
142		elin 3796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( s e. ( x i^i u ) <-> ( s e. x /\ s e. u ) )
143		elunii 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( y e. s /\ s e. ( x i^i u ) ) -> y e. U. ( x i^i u ) )
144	143	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( y e. s -> ( s e. ( x i^i u ) -> y e. U. ( x i^i u ) ) )
145	142, 144	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( y e. s -> ( ( s e. x /\ s e. u ) -> y e. U. ( x i^i u ) ) )
146	145	expd 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( y e. s -> ( s e. x -> ( s e. u -> y e. U. ( x i^i u ) ) ) )
147	137, 141, 146	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> ( s e. u -> y e. U. ( x i^i u ) ) )
148	147	con3d 148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) ) -> ( -. y e. U. ( x i^i u ) -> -. s e. u ) )
149	148	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) ) -> ( ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) -> ( -. y e. U. ( x i^i u ) -> -. s e. u ) ) )
150	149	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ y e. w ) ) -> ( -. y e. U. ( x i^i u ) -> ( ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) -> -. s e. u ) ) )
151	150	exp32 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> ( ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) -> -. s e. u ) ) ) ) )
152	151	imp55 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> -. s e. u )
153		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- s e. _V
154		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = s -> ( v e. ( u u. { s } ) <-> s e. ( u u. { s } ) ) )
155		elequ1 1997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( v = s -> ( v e. u <-> s e. u ) )
156	155	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( v = s -> ( -. v e. u <-> -. s e. u ) )
157	154, 156	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( v = s -> ( ( v e. ( u u. { s } ) /\ -. v e. u ) <-> ( s e. ( u u. { s } ) /\ -. s e. u ) ) )
158	153, 157	spcev 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( s e. ( u u. { s } ) /\ -. s e. u ) -> E. v ( v e. ( u u. { s } ) /\ -. v e. u ) )
159	126, 152, 158	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> E. v ( v e. ( u u. { s } ) /\ -. v e. u ) )
160		nss 3663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( -. ( u u. { s } ) C_ u <-> E. v ( v e. ( u u. { s } ) /\ -. v e. u ) )
161	159, 160	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> -. ( u u. { s } ) C_ u )
162		eqimss2 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( u = ( u u. { s } ) -> ( u u. { s } ) C_ u )
163	162	necon3bi 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( -. ( u u. { s } ) C_ u -> u =/= ( u u. { s } ) )
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> u =/= ( u u. { s } ) )
165	164, 106	jctil 560	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> ( u C_ ( u u. { s } ) /\ u =/= ( u u. { s } ) ) )
166		df-pss 3590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( u C. ( u u. { s } ) <-> ( u C_ ( u u. { s } ) /\ u =/= ( u u. { s } ) ) )
167	165, 166	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> u C. ( u u. { s } ) )
168		psseq2 3695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( v = ( u u. { s } ) -> ( u C. v <-> u C. ( u u. { s } ) ) )
169	168	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( u u. { s } ) e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) /\ u C. ( u u. { s } ) ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
170	123, 167, 169	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) /\ ( s e. t /\ A. n e. ( ~P ( u u. { s } ) i^i Fin ) -. X = U. n ) ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
171	86, 170	rexlimddv 3035	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) /\ ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) /\ ( y e. w /\ -. y e. U. ( x i^i u ) ) ) ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v )
172	171	exp45 642	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( ( t e. ( ~P x i^i Fin ) /\ w = |^| t ) -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) )
173	172	expd 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( t e. ( ~P x i^i Fin ) -> ( w = |^| t -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) ) )
174	173	rexlimdv 3030	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) /\ w e. u ) -> ( E. t e. ( ~P x i^i Fin ) w = |^| t -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) )
175	174	ex 450	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> ( E. t e. ( ~P x i^i Fin ) w = |^| t -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) ) )
176	85, 175	mpdd 43	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( w e. u -> ( y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) ) )
177	176	rexlimdv 3030	. . . . . . . . . . . . . . . . . 18 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( E. w e. u y e. w -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) )
178	78, 177	syl5bi 232	. . . . . . . . . . . . . . . . 17 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( y e. U. u -> ( -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) ) )
179	178	rexlimdv 3030	. . . . . . . . . . . . . . . 16 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( E. y e. U. u -. y e. U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) )
180	77, 179	syl5bi 232	. . . . . . . . . . . . . . 15 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( -. U. u C_ U. ( x i^i u ) -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) )
181	18, 74, 180	3syld 60	. . . . . . . . . . . . . 14 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( X = U. a -> E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v ) )
182	181	con3d 148	. . . . . . . . . . . . 13 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( -. E. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) u C. v -> -. X = U. a ) )
183	14, 182	syl5bi 232	. . . . . . . . . . . 12 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) )
184	183	ex 450	. . . . . . . . . . 11 |- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
185	184	adantr 481	. . . . . . . . . 10 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
186		ssun1 3776	. . . . . . . . . . . . . 14 |- { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } C_ ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } )
187		simpll3 1102	. . . . . . . . . . . . . . 15 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> a e. ~P ( fi ` x ) )
188		simplr 792	. . . . . . . . . . . . . . 15 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> A. b e. ( ~P a i^i Fin ) -. X = U. b )
189		eqimss2 3658	. . . . . . . . . . . . . . . . . 18 |- ( z = a -> a C_ z )
190	189	biantrurd 529	. . . . . . . . . . . . . . . . 17 |- ( z = a -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) ) )
191		pweq 4161	. . . . . . . . . . . . . . . . . . 19 |- ( z = a -> ~P z = ~P a )
192	191	ineq1d 3813	. . . . . . . . . . . . . . . . . 18 |- ( z = a -> ( ~P z i^i Fin ) = ( ~P a i^i Fin ) )
193	192	raleqdv 3144	. . . . . . . . . . . . . . . . 17 |- ( z = a -> ( A. b e. ( ~P z i^i Fin ) -. X = U. b <-> A. b e. ( ~P a i^i Fin ) -. X = U. b ) )
194	190, 193	bitr3d 270	. . . . . . . . . . . . . . . 16 |- ( z = a -> ( ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) <-> A. b e. ( ~P a i^i Fin ) -. X = U. b ) )
195	194	elrab 3363	. . . . . . . . . . . . . . 15 |- ( a e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } <-> ( a e. ~P ( fi ` x ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) )
196	187, 188, 195	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> a e. { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } )
197	186, 196	sseldi 3601	. . . . . . . . . . . . 13 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> a e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) )
198		psseq2 3695	. . . . . . . . . . . . . . 15 |- ( v = a -> ( u C. v <-> u C. a ) )
199	198	notbid 308	. . . . . . . . . . . . . 14 |- ( v = a -> ( -. u C. v <-> -. u C. a ) )
200	199	rspcv 3305	. . . . . . . . . . . . 13 |- ( a e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. u C. a ) )
201	197, 200	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. u C. a ) )
202		id 22	. . . . . . . . . . . . . . . . 17 |- ( a = (/) -> a = (/) )
203		0elpw 4834	. . . . . . . . . . . . . . . . . 18 |- (/) e. ~P a
204		0fin 8188	. . . . . . . . . . . . . . . . . 18 |- (/) e. Fin
205		elin 3796	. . . . . . . . . . . . . . . . . 18 |- ( (/) e. ( ~P a i^i Fin ) <-> ( (/) e. ~P a /\ (/) e. Fin ) )
206	203, 204, 205	mpbir2an 955	. . . . . . . . . . . . . . . . 17 |- (/) e. ( ~P a i^i Fin )
207	202, 206	syl6eqel 2709	. . . . . . . . . . . . . . . 16 |- ( a = (/) -> a e. ( ~P a i^i Fin ) )
208		unieq 4444	. . . . . . . . . . . . . . . . . . 19 |- ( b = a -> U. b = U. a )
209	208	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 |- ( b = a -> ( X = U. b <-> X = U. a ) )
210	209	notbid 308	. . . . . . . . . . . . . . . . 17 |- ( b = a -> ( -. X = U. b <-> -. X = U. a ) )
211	210	rspccv 3306	. . . . . . . . . . . . . . . 16 |- ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> ( a e. ( ~P a i^i Fin ) -> -. X = U. a ) )
212	207, 211	syl5 34	. . . . . . . . . . . . . . 15 |- ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> ( a = (/) -> -. X = U. a ) )
213	212	necon2ad 2809	. . . . . . . . . . . . . 14 |- ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> ( X = U. a -> a =/= (/) ) )
214	213	ad2antlr 763	. . . . . . . . . . . . 13 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( X = U. a -> a =/= (/) ) )
215		psseq1 3694	. . . . . . . . . . . . . . 15 |- ( u = (/) -> ( u C. a <-> (/) C. a ) )
216	215	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( u C. a <-> (/) C. a ) )
217		0pss 4013	. . . . . . . . . . . . . 14 |- ( (/) C. a <-> a =/= (/) )
218	216, 217	syl6bb 276	. . . . . . . . . . . . 13 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( u C. a <-> a =/= (/) ) )
219	214, 218	sylibrd 249	. . . . . . . . . . . 12 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( X = U. a -> u C. a ) )
220	201, 219	nsyld 154	. . . . . . . . . . 11 |- ( ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) /\ u = (/) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) )
221	220	ex 450	. . . . . . . . . 10 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( u = (/) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
222	185, 221	jaod 395	. . . . . . . . 9 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( ( ( u e. ~P ( fi ` x ) /\ ( a C_ u /\ A. b e. ( ~P u i^i Fin ) -. X = U. b ) ) \/ u = (/) ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
223	13, 222	syl5bi 232	. . . . . . . 8 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -> ( A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) ) )
224	223	rexlimdv 3030	. . . . . . 7 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> ( E. u e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) A. v e. ( { z e. ~P ( fi ` x ) | ( a C_ z /\ A. b e. ( ~P z i^i Fin ) -. X = U. b ) } u. { (/) } ) -. u C. v -> -. X = U. a ) )
225	3, 224	mpd 15	. . . . . 6 |- ( ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) /\ A. b e. ( ~P a i^i Fin ) -. X = U. b ) -> -. X = U. a )
226	225	ex 450	. . . . 5 |- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( A. b e. ( ~P a i^i Fin ) -. X = U. b -> -. X = U. a ) )
227	1, 226	syl5bir 233	. . . 4 |- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( -. E. b e. ( ~P a i^i Fin ) X = U. b -> -. X = U. a ) )
228	227	con4d 114	. . 3 |- ( ( J = ( topGen ` ( fi ` x ) ) /\ A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) /\ a e. ~P ( fi ` x ) ) -> ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) )
229	228	3exp 1264	. 2 |- ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> ( a e. ~P ( fi ` x ) -> ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) ) )
230	229	ralrimdv 2968	1 |- ( J = ( topGen ` ( fi ` x ) ) -> ( A. c e. ~P x ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) -> A. a e. ~P ( fi ` x ) ( X = U. a -> E. b e. ( ~P a i^i Fin ) X = U. b ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   u. cun 3572   i^i cin 3573   C_ wss 3574   C. wpss 3575   (/)c0 3915   ~Pcpw 4158   {csn 4177   U.cuni 4436   |^|cint 4475   ` cfv 5888   Fincfn 7955   ficfi 8316   topGenctg 16098   TopBasesctb 20749

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-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-ac2 9285

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-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  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-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-rpss 6937  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-fin 7959  df-fi 8317  df-card 8765  df-ac 8939  df-topgen 16104  df-bases 20750

This theorem is referenced by:  alexsubALT  21855