Theorem alexsublem3 16263

Description: Lemma for alexsub 16265. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover.

Hypothesis

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

Assertion

Ref	Expression
alexsublem3	|- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. 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)

Distinct variable groups:   a,b,c,d,n,s,t,u,w,x,y,J   X,a,b,c,d,n,s,t,u,w,x,y

Proof of Theorem alexsublem3

Step	Hyp	Ref	Expression
1		elin 2999	. . . . . . . . . . . . . . . . . 18 |- (n e. (~P(u u. {s}) i^i Fin) <-> (n e. ~P(u u. {s}) /\ n e. Fin))
2		elpwi 3233	. . . . . . . . . . . . . . . . . . . . . 22 |- (n e. ~P(u u. {s}) -> n C_ (u u. {s}))
3	2	adantr 447	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. ~P(u u. {s}) /\ n e. Fin) -> n C_ (u u. {s}))
4		uncom 2963	. . . . . . . . . . . . . . . . . . . . 21 |- (u u. {s}) = ({s} u. u)
5	3, 4	syl6sseq 2892	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. ~P(u u. {s}) /\ n e. Fin) -> n C_ ({s} u. u))
6		ssundif 3154	. . . . . . . . . . . . . . . . . . . 20 |- (n C_ ({s} u. u) <-> (n \ {s}) C_ u)
7	5, 6	sylib 242	. . . . . . . . . . . . . . . . . . 19 |- ((n e. ~P(u u. {s}) /\ n e. Fin) -> (n \ {s}) C_ u)
8		diffi 5841	. . . . . . . . . . . . . . . . . . . 20 |- (n e. Fin -> (n \ {s}) e. Fin)
9	8	adantl 448	. . . . . . . . . . . . . . . . . . 19 |- ((n e. ~P(u u. {s}) /\ n e. Fin) -> (n \ {s}) e. Fin)
10	7, 9	jca 494	. . . . . . . . . . . . . . . . . 18 |- ((n e. ~P(u u. {s}) /\ n e. Fin) -> ((n \ {s}) C_ u /\ (n \ {s}) e. Fin))
11	1, 10	sylbi 225	. . . . . . . . . . . . . . . . 17 |- (n e. (~P(u u. {s}) i^i Fin) -> ((n \ {s}) C_ u /\ (n \ {s}) e. Fin))
12	11	adantr 447	. . . . . . . . . . . . . . . 16 |- ((n e. (~P(u u. {s}) i^i Fin) /\ X = U.n) -> ((n \ {s}) C_ u /\ (n \ {s}) e. Fin))
13	12	ad2antll 805	. . . . . . . . . . . . . . 15 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> ((n \ {s}) C_ u /\ (n \ {s}) e. Fin))
14		elin 2999	. . . . . . . . . . . . . . . 16 |- ((n \ {s}) e. (~Pu i^i Fin) <-> ((n \ {s}) e. ~Pu /\ (n \ {s}) e. Fin))
15		visset 2541	. . . . . . . . . . . . . . . . . 18 |- u e. _V
16	15	elpw2 3631	. . . . . . . . . . . . . . . . 17 |- ((n \ {s}) e. ~Pu <-> (n \ {s}) C_ u)
17	16	anbi1i 709	. . . . . . . . . . . . . . . 16 |- (((n \ {s}) e. ~Pu /\ (n \ {s}) e. Fin) <-> ((n \ {s}) C_ u /\ (n \ {s}) e. Fin))
18	14, 17	bitr2i 281	. . . . . . . . . . . . . . 15 |- (((n \ {s}) C_ u /\ (n \ {s}) e. Fin) <-> (n \ {s}) e. (~Pu i^i Fin))
19	13, 18	sylib 242	. . . . . . . . . . . . . 14 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> (n \ {s}) e. (~Pu i^i Fin))
20		simprrr 821	. . . . . . . . . . . . . . . 16 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> X = U.n)
21		eldif 2840	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. (n \ {s}) <-> (x e. n /\ -. x e. {s}))
22	21	simplbi2 623	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. n -> (-. x e. {s} -> x e. (n \ {s})))
23		elun 2960	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. ((n \ {s}) u. {s}) <-> (x e. (n \ {s}) \/ x e. {s}))
24		orcom 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. {s} \/ x e. (n \ {s})) <-> (x e. (n \ {s}) \/ x e. {s}))
25		df-or 338	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. {s} \/ x e. (n \ {s})) <-> (-. x e. {s} -> x e. (n \ {s})))
26	23, 24, 25	3bitr2ri 292	. . . . . . . . . . . . . . . . . . . . 21 |- ((-. x e. {s} -> x e. (n \ {s})) <-> x e. ((n \ {s}) u. {s}))
27	22, 26	sylib 242	. . . . . . . . . . . . . . . . . . . 20 |- (x e. n -> x e. ((n \ {s}) u. {s}))
28	27	ssriv 2852	. . . . . . . . . . . . . . . . . . 19 |- n C_ ((n \ {s}) u. {s})
29		uniss 3387	. . . . . . . . . . . . . . . . . . 19 |- (n C_ ((n \ {s}) u. {s}) -> U.n C_ U.((n \ {s}) u. {s}))
30	28, 29	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- U.n C_ U.((n \ {s}) u. {s})
31	30	a1i 8	. . . . . . . . . . . . . . . . 17 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.n C_ U.((n \ {s}) u. {s}))
32		uniun 3385	. . . . . . . . . . . . . . . . . 18 |- U.((n \ {s}) u. {s}) = (U.(n \ {s}) u. U.{s})
33		visset 2541	. . . . . . . . . . . . . . . . . . . 20 |- s e. _V
34	33	unisn 3382	. . . . . . . . . . . . . . . . . . 19 |- U.{s} = s
35	34	uneq2i 2970	. . . . . . . . . . . . . . . . . 18 |- (U.(n \ {s}) u. U.{s}) = (U.(n \ {s}) u. s)
36	32, 35	eqtri 2161	. . . . . . . . . . . . . . . . 17 |- U.((n \ {s}) u. {s}) = (U.(n \ {s}) u. s)
37	31, 36	syl6sseq 2892	. . . . . . . . . . . . . . . 16 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.n C_ (U.(n \ {s}) u. s))
38	20, 37	eqsstrd 2878	. . . . . . . . . . . . . . 15 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> X C_ (U.(n \ {s}) u. s))
39		difss 2954	. . . . . . . . . . . . . . . . . . . . 21 |- (n \ {s}) C_ n
40		uniss 3387	. . . . . . . . . . . . . . . . . . . . 21 |- ((n \ {s}) C_ n -> U.(n \ {s}) C_ U.n)
41	39, 40	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- U.(n \ {s}) C_ U.n
42		sseq2 2866	. . . . . . . . . . . . . . . . . . . 20 |- (X = U.n -> (U.(n \ {s}) C_ X <-> U.(n \ {s}) C_ U.n))
43	41, 42	mpbiri 321	. . . . . . . . . . . . . . . . . . 19 |- (X = U.n -> U.(n \ {s}) C_ X)
44	43	adantl 448	. . . . . . . . . . . . . . . . . 18 |- ((n e. (~P(u u. {s}) i^i Fin) /\ X = U.n) -> U.(n \ {s}) C_ X)
45	44	ad2antll 805	. . . . . . . . . . . . . . . . 17 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.(n \ {s}) C_ X)
46		simpll1 1159	. . . . . . . . . . . . . . . . . . . . 21 |- ((((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u) -> t C_ x)
47	46	ad2antlr 802	. . . . . . . . . . . . . . . . . . . 20 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> t C_ x)
48		simprl 812	. . . . . . . . . . . . . . . . . . . 20 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> s e. t)
49	47, 48	sseldd 2851	. . . . . . . . . . . . . . . . . . 19 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> s e. x)
50		elssuni 3392	. . . . . . . . . . . . . . . . . . 19 |- (s e. x -> s C_ U.x)
51	49, 50	syl 13	. . . . . . . . . . . . . . . . . 18 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> s C_ U.x)
52		visset 2541	. . . . . . . . . . . . . . . . . . . . . . 23 |- x e. _V
53		fibas 11056	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. _V -> ( fi ` x) e. TopBases)
54	52, 53	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . 22 |- ( fi ` x) e. TopBases
55		unitg 9744	. . . . . . . . . . . . . . . . . . . . . 22 |- (( fi ` x) e. TopBases -> U.(topGen` ( fi ` x)) = U.( fi ` x))
56	54, 55	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- U.(topGen` ( fi ` x)) = U.( fi ` x)
57	56	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.(topGen` ( fi ` x)) = U.( fi ` x))
58		unieq 3375	. . . . . . . . . . . . . . . . . . . . . 22 |- (J = (topGen` ( fi ` x)) -> U.J = U.(topGen` ( fi ` x)))
59	58	3ad2ant1 1141	. . . . . . . . . . . . . . . . . . . . 21 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> U.J = U.(topGen` ( fi ` x)))
60	59	ad3antrrr 801	. . . . . . . . . . . . . . . . . . . 20 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.J = U.(topGen` ( fi ` x)))
61		fiuni 11054	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. _V -> U.x = U.( fi ` x))
62	52, 61	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- U.x = U.( fi ` x)
63	62	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.x = U.( fi ` x))
64	57, 60, 63	3eqtr4rd 2184	. . . . . . . . . . . . . . . . . . 19 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.x = U.J)
65		alexsub.1	. . . . . . . . . . . . . . . . . . 19 |- X = U.J
66	64, 65	syl6eqr 2195	. . . . . . . . . . . . . . . . . 18 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> U.x = X)
67	51, 66	sseqtrd 2880	. . . . . . . . . . . . . . . . 17 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> s C_ X)
68	45, 67	jca 494	. . . . . . . . . . . . . . . 16 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> (U.(n \ {s}) C_ X /\ s C_ X))
69		unss 2993	. . . . . . . . . . . . . . . 16 |- ((U.(n \ {s}) C_ X /\ s C_ X) <-> (U.(n \ {s}) u. s) C_ X)
70	68, 69	sylib 242	. . . . . . . . . . . . . . 15 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> (U.(n \ {s}) u. s) C_ X)
71	38, 70	eqssd 2862	. . . . . . . . . . . . . 14 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> X = (U.(n \ {s}) u. s))
72		unieq 3375	. . . . . . . . . . . . . . . . 17 |- (m = (n \ {s}) -> U.m = U.(n \ {s}))
73	72	uneq1d 2972	. . . . . . . . . . . . . . . 16 |- (m = (n \ {s}) -> (U.m u. s) = (U.(n \ {s}) u. s))
74	73	eqeq2d 2152	. . . . . . . . . . . . . . 15 |- (m = (n \ {s}) -> (X = (U.m u. s) <-> X = (U.(n \ {s}) u. s)))
75	74	rcla4ev 2620	. . . . . . . . . . . . . 14 |- (((n \ {s}) e. (~Pu i^i Fin) /\ X = (U.(n \ {s}) u. s)) -> E.m e. (~Pu i^i Fin)X = (U.m u. s))
76	19, 71, 75	syl11anc 659	. . . . . . . . . . . . 13 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (s e. t /\ (n e. (~P(u u. {s}) i^i Fin) /\ X = U.n))) -> E.m e. (~Pu i^i Fin)X = (U.m u. s))
77	76	expr 589	. . . . . . . . . . . 12 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ s e. t) -> ((n e. (~P(u u. {s}) i^i Fin) /\ X = U.n) -> E.m e. (~Pu i^i Fin)X = (U.m u. s)))
78	77	exp3a 400	. . . . . . . . . . 11 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ s e. t) -> (n e. (~P(u u. {s}) i^i Fin) -> (X = U.n -> E.m e. (~Pu i^i Fin)X = (U.m u. s))))
79	78	r19.23adv 2463	. . . . . . . . . 10 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ s e. t) -> (E.n e. (~P(u u. {s}) i^i Fin)X = U.n -> E.m e. (~Pu i^i Fin)X = (U.m u. s)))
80	79	ralimdva 2421	. . . . . . . . 9 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> (A.s e. t E.n e. (~P(u u. {s}) i^i Fin)X = U.n -> A.s e. t E.m e. (~Pu i^i Fin)X = (U.m u. s)))
81		unieq 3375	. . . . . . . . . . . . . . . 16 |- (m = (f` s) -> U.m = U.(f` s))
82	81	uneq1d 2972	. . . . . . . . . . . . . . 15 |- (m = (f` s) -> (U.m u. s) = (U.(f` s) u. s))
83	82	eqeq2d 2152	. . . . . . . . . . . . . 14 |- (m = (f` s) -> (X = (U.m u. s) <-> X = (U.(f` s) u. s)))
84	83	ac6sfi 5675	. . . . . . . . . . . . 13 |- ((t e. Fin /\ A.s e. t E.m e. (~Pu i^i Fin)X = (U.m u. s)) -> E.f(f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s)))
85	84	ex 398	. . . . . . . . . . . 12 |- (t e. Fin -> (A.s e. t E.m e. (~Pu i^i Fin)X = (U.m u. s) -> E.f(f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))))
86	85	3ad2ant2 1142	. . . . . . . . . . 11 |- ((t C_ x /\ t e. Fin /\ w = |^|t) -> (A.s e. t E.m e. (~Pu i^i Fin)X = (U.m u. s) -> E.f(f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))))
87	86	adantr 447	. . . . . . . . . 10 |- (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) -> (A.s e. t E.m e. (~Pu i^i Fin)X = (U.m u. s) -> E.f(f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))))
88	87	ad2antrl 804	. . . . . . . . 9 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> (A.s e. t E.m e. (~Pu i^i Fin)X = (U.m u. s) -> E.f(f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))))
89		ffvelrn 4877	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:t-->(~Pu i^i Fin) /\ s e. t) -> (f` s) e. (~Pu i^i Fin))
90		elin 2999	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` s) e. (~Pu i^i Fin) <-> ((f` s) e. ~Pu /\ (f` s) e. Fin))
91		elpwi 3233	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` s) e. ~Pu -> (f` s) C_ u)
92	91	adantr 447	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f` s) e. ~Pu /\ (f` s) e. Fin) -> (f` s) C_ u)
93	90, 92	sylbi 225	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` s) e. (~Pu i^i Fin) -> (f` s) C_ u)
94	89, 93	syl 13	. . . . . . . . . . . . . . . . . . . 20 |- ((f:t-->(~Pu i^i Fin) /\ s e. t) -> (f` s) C_ u)
95	94	ex 398	. . . . . . . . . . . . . . . . . . 19 |- (f:t-->(~Pu i^i Fin) -> (s e. t -> (f` s) C_ u))
96	95	r19.21aiv 2425	. . . . . . . . . . . . . . . . . 18 |- (f:t-->(~Pu i^i Fin) -> A.s e. t (f` s) C_ u)
97		iunss 3467	. . . . . . . . . . . . . . . . . 18 |- (U_s e. t (f` s) C_ u <-> A.s e. t (f` s) C_ u)
98	96, 97	sylibr 243	. . . . . . . . . . . . . . . . 17 |- (f:t-->(~Pu i^i Fin) -> U_s e. t (f` s) C_ u)
99	98	ad2antrl 804	. . . . . . . . . . . . . . . 16 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> U_s e. t (f` s) C_ u)
100		simplrr 817	. . . . . . . . . . . . . . . . 17 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> w e. u)
101	100	snssd 3323	. . . . . . . . . . . . . . . 16 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> {w} C_ u)
102	99, 101	jca 494	. . . . . . . . . . . . . . 15 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (U_s e. t (f` s) C_ u /\ {w} C_ u))
103		unss 2993	. . . . . . . . . . . . . . 15 |- ((U_s e. t (f` s) C_ u /\ {w} C_ u) <-> (U_s e. t (f` s) u. {w}) C_ u)
104	102, 103	sylib 242	. . . . . . . . . . . . . 14 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (U_s e. t (f` s) u. {w}) C_ u)
105		inss2 3027	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (~Pu i^i Fin) C_ Fin
106	105	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:t-->(~Pu i^i Fin) /\ s e. t) -> (~Pu i^i Fin) C_ Fin)
107	106, 89	sseldd 2851	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f:t-->(~Pu i^i Fin) /\ s e. t) -> (f` s) e. Fin)
108	107	ex 398	. . . . . . . . . . . . . . . . . . . . 21 |- (f:t-->(~Pu i^i Fin) -> (s e. t -> (f` s) e. Fin))
109	108	r19.21aiv 2425	. . . . . . . . . . . . . . . . . . . 20 |- (f:t-->(~Pu i^i Fin) -> A.s e. t (f` s) e. Fin)
110		iunfi 5883	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. Fin /\ A.s e. t (f` s) e. Fin) -> U_s e. t (f` s) e. Fin)
111	109, 110	sylan2 600	. . . . . . . . . . . . . . . . . . 19 |- ((t e. Fin /\ f:t-->(~Pu i^i Fin)) -> U_s e. t (f` s) e. Fin)
112	111	3ad2antl2 1289	. . . . . . . . . . . . . . . . . 18 |- (((t C_ x /\ t e. Fin /\ w = |^|t) /\ f:t-->(~Pu i^i Fin)) -> U_s e. t (f` s) e. Fin)
113	112	adantlr 777	. . . . . . . . . . . . . . . . 17 |- ((((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ f:t-->(~Pu i^i Fin)) -> U_s e. t (f` s) e. Fin)
114	113	adantlr 777	. . . . . . . . . . . . . . . 16 |- (((((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u) /\ f:t-->(~Pu i^i Fin)) -> U_s e. t (f` s) e. Fin)
115	114	ad2ant2lr 808	. . . . . . . . . . . . . . 15 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> U_s e. t (f` s) e. Fin)
116		snfi 5654	. . . . . . . . . . . . . . 15 |- {w} e. Fin
117		unfi 5863	. . . . . . . . . . . . . . 15 |- ((U_s e. t (f` s) e. Fin /\ {w} e. Fin) -> (U_s e. t (f` s) u. {w}) e. Fin)
118	115, 116, 117	sylancl 660	. . . . . . . . . . . . . 14 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (U_s e. t (f` s) u. {w}) e. Fin)
119	104, 118	jca 494	. . . . . . . . . . . . 13 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> ((U_s e. t (f` s) u. {w}) C_ u /\ (U_s e. t (f` s) u. {w}) e. Fin))
120		elin 2999	. . . . . . . . . . . . . 14 |- ((U_s e. t (f` s) u. {w}) e. (~Pu i^i Fin) <-> ((U_s e. t (f` s) u. {w}) e. ~Pu /\ (U_s e. t (f` s) u. {w}) e. Fin))
121	15	elpw2 3631	. . . . . . . . . . . . . . 15 |- ((U_s e. t (f` s) u. {w}) e. ~Pu <-> (U_s e. t (f` s) u. {w}) C_ u)
122	121	anbi1i 709	. . . . . . . . . . . . . 14 |- (((U_s e. t (f` s) u. {w}) e. ~Pu /\ (U_s e. t (f` s) u. {w}) e. Fin) <-> ((U_s e. t (f` s) u. {w}) C_ u /\ (U_s e. t (f` s) u. {w}) e. Fin))
123	120, 122	bitr2i 281	. . . . . . . . . . . . 13 |- (((U_s e. t (f` s) u. {w}) C_ u /\ (U_s e. t (f` s) u. {w}) e. Fin) <-> (U_s e. t (f` s) u. {w}) e. (~Pu i^i Fin))
124	119, 123	sylib 242	. . . . . . . . . . . 12 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (U_s e. t (f` s) u. {w}) e. (~Pu i^i Fin))
125		ralnex 2363	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.s e. t -. y e. (f` s) <-> -. E.s e. t y e. (f` s))
126	125	imbi2i 297	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((v e. y -> A.s e. t -. y e. (f` s)) <-> (v e. y -> -. E.s e. t y e. (f` s)))
127	126	albii 1635	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.y(v e. y -> A.s e. t -. y e. (f` s)) <-> A.y(v e. y -> -. E.s e. t y e. (f` s)))
128		alinexa 1678	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.y(v e. y -> -. E.s e. t y e. (f` s)) <-> -. E.y(v e. y /\ E.s e. t y e. (f` s)))
129	127, 128	bitr2i 281	. . . . . . . . . . . . . . . . . . . . . 22 |- (-. E.y(v e. y /\ E.s e. t y e. (f` s)) <-> A.y(v e. y -> A.s e. t -. y e. (f` s)))
130		fveq2 4765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (s = z -> (f` s) = (f` z))
131	130	unieqd 3377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (s = z -> U.(f` s) = U.(f` z))
132		id 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (s = z -> s = z)
133	131, 132	uneq12d 2974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (s = z -> (U.(f` s) u. s) = (U.(f` z) u. z))
134	133	eqeq2d 2152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (s = z -> (X = (U.(f` s) u. s) <-> X = (U.(f` z) u. z)))
135	134	rcla4v 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (z e. t -> (A.s e. t X = (U.(f` s) u. s) -> X = (U.(f` z) u. z)))
136		eleq2 2205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (X = (U.(f` z) u. z) -> (v e. X <-> v e. (U.(f` z) u. z)))
137	136	biimpd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (X = (U.(f` z) u. z) -> (v e. X -> v e. (U.(f` z) u. z)))
138		elun 2960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v e. (U.(f` z) u. z) <-> (v e. U.(f` z) \/ v e. z))
139		eluni 3369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v e. U.(f` z) <-> E.w(v e. w /\ w e. (f` z)))
140	139	orbi1i 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((v e. U.(f` z) \/ v e. z) <-> (E.w(v e. w /\ w e. (f` z)) \/ v e. z))
141		df-or 338	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((E.w(v e. w /\ w e. (f` z)) \/ v e. z) <-> (-. E.w(v e. w /\ w e. (f` z)) -> v e. z))
142		alinexa 1678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.w(v e. w -> -. w e. (f` z)) <-> -. E.w(v e. w /\ w e. (f` z)))
143	142	imbi1i 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((A.w(v e. w -> -. w e. (f` z)) -> v e. z) <-> (-. E.w(v e. w /\ w e. (f` z)) -> v e. z))
144	141, 143	bitr4i 283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((E.w(v e. w /\ w e. (f` z)) \/ v e. z) <-> (A.w(v e. w -> -. w e. (f` z)) -> v e. z))
145	138, 140, 144	3bitri 289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (v e. (U.(f` z) u. z) <-> (A.w(v e. w -> -. w e. (f` z)) -> v e. z))
146		eleq2 2205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y = w -> (v e. y <-> v e. w))
147		eleq1 2204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = w -> (y e. (f` s) <-> w e. (f` s)))
148	147	notbid 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = w -> (-. y e. (f` s) <-> -. w e. (f` s)))
149	148	ralbidv 2373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y = w -> (A.s e. t -. y e. (f` s) <-> A.s e. t -. w e. (f` s)))
150	146, 149	imbi12d 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (y = w -> ((v e. y -> A.s e. t -. y e. (f` s)) <-> (v e. w -> A.s e. t -. w e. (f` s))))
151	150	a4v 1919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> (v e. w -> A.s e. t -. w e. (f` s)))
152	130	eleq2d 2211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (s = z -> (w e. (f` s) <-> w e. (f` z)))
153	152	notbid 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (s = z -> (-. w e. (f` s) <-> -. w e. (f` z)))
154	153	rcla4v 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (z e. t -> (A.s e. t -. w e. (f` s) -> -. w e. (f` z)))
155	151, 154	syl9r 58	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (z e. t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> (v e. w -> -. w e. (f` z))))
156	155	19.21adv 1935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (z e. t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> A.w(v e. w -> -. w e. (f` z))))
157	156	imim1d 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (z e. t -> ((A.w(v e. w -> -. w e. (f` z)) -> v e. z) -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z)))
158	145, 157	syl5bi 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z e. t -> (v e. (U.(f` z) u. z) -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z)))
159	158	a1dd 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z e. t -> (v e. (U.(f` z) u. z) -> (w = |^|t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z))))
160	137, 159	syl9r 58	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (z e. t -> (X = (U.(f` z) u. z) -> (v e. X -> (w = |^|t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z)))))
161	135, 160	syld 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z e. t -> (A.s e. t X = (U.(f` s) u. s) -> (v e. X -> (w = |^|t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z)))))
162	161	com14 80	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = |^|t -> (A.s e. t X = (U.(f` s) u. s) -> (v e. X -> (z e. t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z)))))
163	162	imp31 396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (z e. t -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. z)))
164	163	com23 65	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> (z e. t -> v e. z)))
165	164	r19.21adv 2431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> A.z e. t v e. z))
166		visset 2541	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- v e. _V
167	166	elint2 3407	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. |^|t <-> A.z e. t v e. z)
168	165, 167	syl6ibr 262	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. |^|t))
169		eleq2 2205	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = |^|t -> (v e. w <-> v e. |^|t))
170	169	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (v e. w <-> v e. |^|t))
171	168, 170	sylibrd 247	. . . . . . . . . . . . . . . . . . . . . 22 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (A.y(v e. y -> A.s e. t -. y e. (f` s)) -> v e. w))
172	129, 171	syl5bi 249	. . . . . . . . . . . . . . . . . . . . 21 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (-. E.y(v e. y /\ E.s e. t y e. (f` s)) -> v e. w))
173	172	orrd 346	. . . . . . . . . . . . . . . . . . . 20 |- (((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) /\ v e. X) -> (E.y(v e. y /\ E.s e. t y e. (f` s)) \/ v e. w))
174	173	ex 398	. . . . . . . . . . . . . . . . . . 19 |- ((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) -> (v e. X -> (E.y(v e. y /\ E.s e. t y e. (f` s)) \/ v e. w)))
175		orc 376	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.s e. t y e. (f` s) -> (E.s e. t y e. (f` s) \/ y = w))
176	175	anim2i 539	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v e. y /\ E.s e. t y e. (f` s)) -> (v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
177	176	eximi 1676	. . . . . . . . . . . . . . . . . . . . 21 |- (E.y(v e. y /\ E.s e. t y e. (f` s)) -> E.y(v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
178		eqid 2141	. . . . . . . . . . . . . . . . . . . . . . 23 |- w = w
179		visset 2541	. . . . . . . . . . . . . . . . . . . . . . . 24 |- w e. _V
180		eqeq1 2147	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = w -> (y = w <-> w = w))
181	146, 180	anbi12d 763	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = w -> ((v e. y /\ y = w) <-> (v e. w /\ w = w)))
182	179, 181	cla4ev 2611	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. w /\ w = w) -> E.y(v e. y /\ y = w))
183	178, 182	mpan2 679	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. w -> E.y(v e. y /\ y = w))
184		olc 375	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = w -> (E.s e. t y e. (f` s) \/ y = w))
185	184	anim2i 539	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. y /\ y = w) -> (v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
186	185	eximi 1676	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.y(v e. y /\ y = w) -> E.y(v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
187	183, 186	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (v e. w -> E.y(v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
188	177, 187	jaoi 453	. . . . . . . . . . . . . . . . . . . 20 |- ((E.y(v e. y /\ E.s e. t y e. (f` s)) \/ v e. w) -> E.y(v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
189		eluni 3369	. . . . . . . . . . . . . . . . . . . . 21 |- (v e. U.(U_s e. t (f` s) u. {w}) <-> E.y(v e. y /\ y e. (U_s e. t (f` s) u. {w})))
190		elun 2960	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. (U_s e. t (f` s) u. {w}) <-> (y e. U_s e. t (f` s) \/ y e. {w}))
191		eliun 3440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. U_s e. t (f` s) <-> E.s e. t y e. (f` s))
192		elsn 3251	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. {w} <-> y = w)
193	191, 192	orbi12i 479	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((y e. U_s e. t (f` s) \/ y e. {w}) <-> (E.s e. t y e. (f` s) \/ y = w))
194	190, 193	bitri 279	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. (U_s e. t (f` s) u. {w}) <-> (E.s e. t y e. (f` s) \/ y = w))
195	194	anbi2i 708	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v e. y /\ y e. (U_s e. t (f` s) u. {w})) <-> (v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
196	195	exbii 1687	. . . . . . . . . . . . . . . . . . . . 21 |- (E.y(v e. y /\ y e. (U_s e. t (f` s) u. {w})) <-> E.y(v e. y /\ (E.s e. t y e. (f` s) \/ y = w)))
197	189, 196	bitr2i 281	. . . . . . . . . . . . . . . . . . . 20 |- (E.y(v e. y /\ (E.s e. t y e. (f` s) \/ y = w)) <-> v e. U.(U_s e. t (f` s) u. {w}))
198	188, 197	sylib 242	. . . . . . . . . . . . . . . . . . 19 |- ((E.y(v e. y /\ E.s e. t y e. (f` s)) \/ v e. w) -> v e. U.(U_s e. t (f` s) u. {w}))
199	174, 198	syl6 42	. . . . . . . . . . . . . . . . . 18 |- ((w = |^|t /\ A.s e. t X = (U.(f` s) u. s)) -> (v e. X -> v e. U.(U_s e. t (f` s) u. {w})))
200	199	3ad2antl3 1290	. . . . . . . . . . . . . . . . 17 |- (((t C_ x /\ t e. Fin /\ w = |^|t) /\ A.s e. t X = (U.(f` s) u. s)) -> (v e. X -> v e. U.(U_s e. t (f` s) u. {w})))
201	200	adantlr 777	. . . . . . . . . . . . . . . 16 |- ((((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ A.s e. t X = (U.(f` s) u. s)) -> (v e. X -> v e. U.(U_s e. t (f` s) u. {w})))
202	201	adantlr 777	. . . . . . . . . . . . . . 15 |- (((((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u) /\ A.s e. t X = (U.(f` s) u. s)) -> (v e. X -> v e. U.(U_s e. t (f` s) u. {w})))
203	202	ad2ant2l 806	. . . . . . . . . . . . . 14 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (v e. X -> v e. U.(U_s e. t (f` s) u. {w})))
204	203	ssrdv 2853	. . . . . . . . . . . . 13 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> X C_ U.(U_s e. t (f` s) u. {w}))
205		elun 2960	. . . . . . . . . . . . . . . . 17 |- (v e. (U_s e. t (f` s) u. {w}) <-> (v e. U_s e. t (f` s) \/ v e. {w}))
206		eliun 3440	. . . . . . . . . . . . . . . . . 18 |- (v e. U_s e. t (f` s) <-> E.s e. t v e. (f` s))
207		elsn 3251	. . . . . . . . . . . . . . . . . 18 |- (v e. {w} <-> v = w)
208	206, 207	orbi12i 479	. . . . . . . . . . . . . . . . 17 |- ((v e. U_s e. t (f` s) \/ v e. {w}) <-> (E.s e. t v e. (f` s) \/ v = w))
209	205, 208	bitri 279	. . . . . . . . . . . . . . . 16 |- (v e. (U_s e. t (f` s) u. {w}) <-> (E.s e. t v e. (f` s) \/ v = w))
210		hbra1 2398	. . . . . . . . . . . . . . . . . . 19 |- (A.s e. t X = (U.(f` s) u. s) -> A.sA.s e. t X = (U.(f` s) u. s))
211		ax-17 1605	. . . . . . . . . . . . . . . . . . 19 |- (v C_ X -> A.s v C_ X)
212		ra4 2406	. . . . . . . . . . . . . . . . . . . 20 |- (A.s e. t X = (U.(f` s) u. s) -> (s e. t -> X = (U.(f` s) u. s)))
213		eqimss2 2895	. . . . . . . . . . . . . . . . . . . . 21 |- (X = (U.(f` s) u. s) -> (U.(f` s) u. s) C_ X)
214		elssuni 3392	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. (f` s) -> v C_ U.(f` s))
215		ssun3 2984	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v C_ U.(f` s) -> v C_ (U.(f` s) u. s))
216	214, 215	syl 13	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. (f` s) -> v C_ (U.(f` s) u. s))
217		sstr 2855	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v C_ (U.(f` s) u. s) /\ (U.(f` s) u. s) C_ X) -> v C_ X)
218	217	expcom 399	. . . . . . . . . . . . . . . . . . . . . 22 |- ((U.(f` s) u. s) C_ X -> (v C_ (U.(f` s) u. s) -> v C_ X))
219	216, 218	syl5 35	. . . . . . . . . . . . . . . . . . . . 21 |- ((U.(f` s) u. s) C_ X -> (v e. (f` s) -> v C_ X))
220	213, 219	syl 13	. . . . . . . . . . . . . . . . . . . 20 |- (X = (U.(f` s) u. s) -> (v e. (f` s) -> v C_ X))
221	212, 220	syl6 42	. . . . . . . . . . . . . . . . . . 19 |- (A.s e. t X = (U.(f` s) u. s) -> (s e. t -> (v e. (f` s) -> v C_ X)))
222	210, 211, 221	r19.23ad 2462	. . . . . . . . . . . . . . . . . 18 |- (A.s e. t X = (U.(f` s) u. s) -> (E.s e. t v e. (f` s) -> v C_ X))
223	222	ad2antll 805	. . . . . . . . . . . . . . . . 17 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (E.s e. t v e. (f` s) -> v C_ X))
224		elpwi 3233	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. ~P( fi ` x) -> u C_ ( fi ` x))
225	224	ad2antrl 804	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) -> u C_ ( fi ` x))
226	225	ad2antrr 799	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> u C_ ( fi ` x))
227	226, 100	sseldd 2851	. . . . . . . . . . . . . . . . . . . 20 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> w e. ( fi ` x))
228		elssuni 3392	. . . . . . . . . . . . . . . . . . . 20 |- (w e. ( fi ` x) -> w C_ U.( fi ` x))
229	227, 228	syl 13	. . . . . . . . . . . . . . . . . . 19 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> w C_ U.( fi ` x))
230	58, 56	syl6req 2194	. . . . . . . . . . . . . . . . . . . . . 22 |- (J = (topGen` ( fi ` x)) -> U.( fi ` x) = U.J)
231	230, 65	syl6eqr 2195	. . . . . . . . . . . . . . . . . . . . 21 |- (J = (topGen` ( fi ` x)) -> U.( fi ` x) = X)
232	231	3ad2ant1 1141	. . . . . . . . . . . . . . . . . . . 20 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> U.( fi ` x) = X)
233	232	ad3antrrr 801	. . . . . . . . . . . . . . . . . . 19 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> U.( fi ` x) = X)
234	229, 233	sseqtrd 2880	. . . . . . . . . . . . . . . . . 18 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> w C_ X)
235		sseq1 2865	. . . . . . . . . . . . . . . . . 18 |- (v = w -> (v C_ X <-> w C_ X))
236	234, 235	syl5ibrcom 258	. . . . . . . . . . . . . . . . 17 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (v = w -> v C_ X))
237	223, 236	jaod 454	. . . . . . . . . . . . . . . 16 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> ((E.s e. t v e. (f` s) \/ v = w) -> v C_ X))
238	209, 237	syl5bi 249	. . . . . . . . . . . . . . 15 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> (v e. (U_s e. t (f` s) u. {w}) -> v C_ X))
239	238	r19.21aiv 2425	. . . . . . . . . . . . . 14 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> A.v e. (U_s e. t (f` s) u. {w})v C_ X)
240		unissb 3394	. . . . . . . . . . . . . 14 |- (U.(U_s e. t (f` s) u. {w}) C_ X <-> A.v e. (U_s e. t (f` s) u. {w})v C_ X)
241	239, 240	sylibr 243	. . . . . . . . . . . . 13 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> U.(U_s e. t (f` s) u. {w}) C_ X)
242	204, 241	eqssd 2862	. . . . . . . . . . . 12 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> X = U.(U_s e. t (f` s) u. {w}))
243		unieq 3375	. . . . . . . . . . . . . 14 |- (b = (U_s e. t (f` s) u. {w}) -> U.b = U.(U_s e. t (f` s) u. {w}))
244	243	eqeq2d 2152	. . . . . . . . . . . . 13 |- (b = (U_s e. t (f` s) u. {w}) -> (X = U.b <-> X = U.(U_s e. t (f` s) u. {w})))
245	244	rcla4ev 2620	. . . . . . . . . . . 12 |- (((U_s e. t (f` s) u. {w}) e. (~Pu i^i Fin) /\ X = U.(U_s e. t (f` s) u. {w})) -> E.b e. (~Pu i^i Fin)X = U.b)
246	124, 242, 245	syl11anc 659	. . . . . . . . . . 11 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) /\ (f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s))) -> E.b e. (~Pu i^i Fin)X = U.b)
247	246	ex 398	. . . . . . . . . 10 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> ((f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s)) -> E.b e. (~Pu i^i Fin)X = U.b))
248	247	19.23adv 1860	. . . . . . . . 9 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> (E.f(f:t-->(~Pu i^i Fin) /\ A.s e. t X = (U.(f` s) u. s)) -> E.b e. (~Pu i^i Fin)X = U.b))
249	80, 88, 248	3syld 59	. . . . . . . 8 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> (A.s e. t E.n e. (~P(u u. {s}) i^i Fin)X = U.n -> E.b e. (~Pu i^i Fin)X = U.b))
250		dfrex2 2366	. . . . . . . . . 10 |- (E.n e. (~P(u u. {s}) i^i Fin)X = U.n <-> -. A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)
251	250	ralbii 2377	. . . . . . . . 9 |- (A.s e. t E.n e. (~P(u u. {s}) i^i Fin)X = U.n <-> A.s e. t -. A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)
252		ralnex 2363	. . . . . . . . 9 |- (A.s e. t -. A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n <-> -. E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n)
253	251, 252	bitr2i 281	. . . . . . . 8 |- (-. E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n <-> A.s e. t E.n e. (~P(u u. {s}) i^i Fin)X = U.n)
254		dfrex2 2366	. . . . . . . . 9 |- (E.b e. (~Pu i^i Fin)X = U.b <-> -. A.b e. (~Pu i^i Fin) -. X = U.b)
255	254	bicomi 268	. . . . . . . 8 |- (-. A.b e. (~Pu i^i Fin) -. X = U.b <-> E.b e. (~Pu i^i Fin)X = U.b)
256	249, 253, 255	3imtr4g 332	. . . . . . 7 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> (-. E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n -> -. A.b e. (~Pu i^i Fin) -. X = U.b))
257	256	con4d 122	. . . . . 6 |- ((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) /\ (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) /\ w e. u)) -> (A.b e. (~Pu i^i Fin) -. X = U.b -> E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))
258	257	exp32 578	. . . . 5 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) -> (((t C_ x /\ t e. Fin /\ w = |^|t) /\ (y e. w /\ -. y e. U.(x i^i u))) -> (w e. u -> (A.b e. (~Pu i^i Fin) -. X = U.b -> E.s e. t A.n e. (~P(u u. {s}) i^i Fin) -. X = U.n))))
259	258	com24 79	. . . 4 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ a C_ u)) -> (A.b e. (~Pu i^i Fin) -. X = U.b -> (w e. u -> (((t C_ x /\ t e. 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))))
260	259	exp32 578	. . 3 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) -> (u e. ~P( fi ` x) -> (a C_ u -> (A.b e. (~Pu i^i Fin) -. X = U.b -> (w e. u -> (((t C_ x /\ t e. 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))))))
261	260	imp45 573	. 2 |- (((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) -> (w e. u -> (((t C_ x /\ t e. 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)))
262	261	imp31 396	1 |- (((((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) /\ a e. ~P( fi ` x)) /\ (u e. ~P( fi ` x) /\ (a C_ u /\ A.b e. (~Pu i^i Fin) -. X = U.b))) /\ w e. u) /\ ((t C_ x /\ t e. 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)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337   /\ w3a 1102  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615  A.wral 2355  E.wrex 2356  _Vcvv 2538   \ cdif 2824   u. cun 2825   i^i cin 2826   C_ wss 2827  ~Pcpw 3227  {csn 3238  U.cuni 3366  |^|cint 3400  U_ciun 3436  -->wf 4127  ` cfv 4131  Fincfn 5587  TopBasesctb 9690  topGenctg 9691   fi cfi 11042

This theorem is referenced by:  alexsublem4 16264

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-rdg 5304  df-1o 5344  df-oadd 5346  df-er 5479  df-en 5588  df-dom 5589  df-fin 5591  df-bases 9694  df-topgen 9695  df-fi 11043

Copyright terms: Public domain