Theorem alexsub 15441

Description: The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover.

Hypothesis

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

Assertion

Ref	Expression
alexsub	|- (J e. Comp <-> E.x(J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d)))

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

Proof of Theorem alexsub

Step	Hyp	Ref	Expression
1		alexsub.1	. . 3 |- X = U.J
2	1	alexsublem1 15437	. 2 |- (J e. Comp -> E.x(J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d)))
3	1	alexsublem4 15440	. . . . 5 |- (J = (topGen` ( fi ` x)) -> (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b)))
4		ssrab2 2692	. . . . . . . . . . . . . . . 16 |- {y e. ( fi ` x) | E.z e. c y C_ z} C_ ( fi ` x)
5		fvex 4689	. . . . . . . . . . . . . . . . 17 |- ( fi ` x) e. _V
6	5	elpw2 3464	. . . . . . . . . . . . . . . 16 |- ({y e. ( fi ` x) | E.z e. c y C_ z} e. ~P( fi ` x) <-> {y e. ( fi ` x) | E.z e. c y C_ z} C_ ( fi ` x))
7	4, 6	mpbir 207	. . . . . . . . . . . . . . 15 |- {y e. ( fi ` x) | E.z e. c y C_ z} e. ~P( fi ` x)
8		unieq 3185	. . . . . . . . . . . . . . . . . 18 |- (a = {y e. ( fi ` x) | E.z e. c y C_ z} -> U.a = U.{y e. ( fi ` x) | E.z e. c y C_ z})
9	8	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (a = {y e. ( fi ` x) | E.z e. c y C_ z} -> (X = U.a <-> X = U.{y e. ( fi ` x) | E.z e. c y C_ z}))
10		pweq 3036	. . . . . . . . . . . . . . . . . . 19 |- (a = {y e. ( fi ` x) | E.z e. c y C_ z} -> ~Pa = ~P{y e. ( fi ` x) | E.z e. c y C_ z})
11	10	ineq1d 2795	. . . . . . . . . . . . . . . . . 18 |- (a = {y e. ( fi ` x) | E.z e. c y C_ z} -> (~Pa i^i Fin) = (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin))
12	11	rexeqdv 2270	. . . . . . . . . . . . . . . . 17 |- (a = {y e. ( fi ` x) | E.z e. c y C_ z} -> (E.b e. (~Pa i^i Fin)X = U.b <-> E.b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin)X = U.b))
13	9, 12	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (a = {y e. ( fi ` x) | E.z e. c y C_ z} -> ((X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) <-> (X = U.{y e. ( fi ` x) | E.z e. c y C_ z} -> E.b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin)X = U.b)))
14	13	rcla4v 2376	. . . . . . . . . . . . . . 15 |- ({y e. ( fi ` x) | E.z e. c y C_ z} e. ~P( fi ` x) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> (X = U.{y e. ( fi ` x) | E.z e. c y C_ z} -> E.b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin)X = U.b)))
15	7, 14	ax-mp 7	. . . . . . . . . . . . . 14 |- (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> (X = U.{y e. ( fi ` x) | E.z e. c y C_ z} -> E.b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin)X = U.b))
16		eleq2 1958	. . . . . . . . . . . . . . . . . . . 20 |- (U.J = U.c -> (t e. U.J <-> t e. U.c))
17	16	3ad2ant3 899	. . . . . . . . . . . . . . . . . . 19 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. U.J <-> t e. U.c))
18		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (c C_ J -> (w e. c -> w e. J))
19		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (J = (topGen` ( fi ` x)) -> (w e. J <-> w e. (topGen` ( fi ` x))))
20		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- x e. _V
21		fibas 10221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x e. _V -> ( fi ` x) e. Bases)
22	20, 21	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( fi ` x) e. Bases
23		tg2 8891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((( fi ` x) e. Bases /\ w e. (topGen` ( fi ` x)) /\ t e. w) -> E.y e. ( fi ` x)(t e. y /\ y C_ w))
24	23	3expia 1069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((( fi ` x) e. Bases /\ w e. (topGen` ( fi ` x))) -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ y C_ w)))
25	22, 24	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. (topGen` ( fi ` x)) -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ y C_ w)))
26	19, 25	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (J = (topGen` ( fi ` x)) -> (w e. J -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ y C_ w))))
27	18, 26	sylan9r 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((J = (topGen` ( fi ` x)) /\ c C_ J) -> (w e. c -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ y C_ w))))
28	27	3impia 1064	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ w e. c) -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ y C_ w)))
29		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z = w -> (y C_ z <-> y C_ w))
30	29	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((w e. c /\ y C_ w) -> E.z e. c y C_ z)
31	30	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. c -> (y C_ w -> E.z e. c y C_ z))
32	31	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ w e. c) -> (y C_ w -> E.z e. c y C_ z))
33	32	anim2d 620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ w e. c) -> ((t e. y /\ y C_ w) -> (t e. y /\ E.z e. c y C_ z)))
34	33	reximdv 2202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ w e. c) -> (E.y e. ( fi ` x)(t e. y /\ y C_ w) -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
35	28, 34	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ w e. c) -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
36	35	3expia 1069	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J = (topGen` ( fi ` x)) /\ c C_ J) -> (w e. c -> (t e. w -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z))))
37	36	com23 36	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J = (topGen` ( fi ` x)) /\ c C_ J) -> (t e. w -> (w e. c -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z))))
38	37	imp3a 388	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J = (topGen` ( fi ` x)) /\ c C_ J) -> ((t e. w /\ w e. c) -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
39	38	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . 21 |- ((J = (topGen` ( fi ` x)) /\ c C_ J) -> (E.w(t e. w /\ w e. c) -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
40		eluni 3180	. . . . . . . . . . . . . . . . . . . . 21 |- (t e. U.c <-> E.w(t e. w /\ w e. c))
41	39, 40	syl5ib 223	. . . . . . . . . . . . . . . . . . . 20 |- ((J = (topGen` ( fi ` x)) /\ c C_ J) -> (t e. U.c -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
42	41	3adant3 896	. . . . . . . . . . . . . . . . . . 19 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. U.c -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
43	17, 42	sylbid 220	. . . . . . . . . . . . . . . . . 18 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. U.J -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
44	1	eleq2i 1961	. . . . . . . . . . . . . . . . . 18 |- (t e. X <-> t e. U.J)
45	43, 44	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. X -> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
46		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y C_ z -> (t e. y -> t e. z))
47		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t e. z /\ z e. c) -> t e. U.c)
48	47	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. c -> (t e. z -> t e. U.c))
49	17, 44	syl5rbb 592	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. U.c <-> t e. X))
50	49	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. U.c -> t e. X))
51	48, 50	sylan9r 519	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ z e. c) -> (t e. z -> t e. X))
52	46, 51	syl9r 72	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ z e. c) -> (y C_ z -> (t e. y -> t e. X)))
53	52	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (z e. c -> (y C_ z -> (t e. y -> t e. X))))
54	53	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . 21 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (E.z e. c y C_ z -> (t e. y -> t e. X)))
55	54	com23 36	. . . . . . . . . . . . . . . . . . . 20 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. y -> (E.z e. c y C_ z -> t e. X)))
56	55	imp3a 388	. . . . . . . . . . . . . . . . . . 19 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> ((t e. y /\ E.z e. c y C_ z) -> t e. X))
57	56	a1d 15	. . . . . . . . . . . . . . . . . 18 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (y e. ( fi ` x) -> ((t e. y /\ E.z e. c y C_ z) -> t e. X)))
58	57	r19.23adv 2215	. . . . . . . . . . . . . . . . 17 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z) -> t e. X))
59	45, 58	impbid 574	. . . . . . . . . . . . . . . 16 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. X <-> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z)))
60		elunirab 3190	. . . . . . . . . . . . . . . 16 |- (t e. U.{y e. ( fi ` x) | E.z e. c y C_ z} <-> E.y e. ( fi ` x)(t e. y /\ E.z e. c y C_ z))
61	59, 60	syl6bbr 597	. . . . . . . . . . . . . . 15 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (t e. X <-> t e. U.{y e. ( fi ` x) | E.z e. c y C_ z}))
62	61	eqrdv 1882	. . . . . . . . . . . . . 14 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> X = U.{y e. ( fi ` x) | E.z e. c y C_ z})
63	15, 62	syl5com 63	. . . . . . . . . . . . 13 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> E.b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin)X = U.b))
64		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z = (f` t) -> (t C_ z <-> t C_ (f` t)))
65	64	ac6sfi 5509	. . . . . . . . . . . . . . . . . . . . . 22 |- ((b e. Fin /\ A.t e. b E.z e. c t C_ z) -> E.f(f:b-->c /\ A.t e. b t C_ (f` t)))
66	65	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- (b e. Fin -> (A.t e. b E.z e. c t C_ z -> E.f(f:b-->c /\ A.t e. b t C_ (f` t))))
67		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> (t e. b -> t e. {y e. ( fi ` x) | E.z e. c y C_ z}))
68		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = t -> (y C_ z <-> t C_ z))
69	68	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = t -> (E.z e. c y C_ z <-> E.z e. c t C_ z))
70	69	elrab 2414	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (t e. {y e. ( fi ` x) | E.z e. c y C_ z} <-> (t e. ( fi ` x) /\ E.z e. c t C_ z))
71	70	simprbi 353	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t e. {y e. ( fi ` x) | E.z e. c y C_ z} -> E.z e. c t C_ z)
72	67, 71	syl6 25	. . . . . . . . . . . . . . . . . . . . . 22 |- (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> (t e. b -> E.z e. c t C_ z))
73	72	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . . 21 |- (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> A.t e. b E.z e. c t C_ z)
74	66, 73	syl5 20	. . . . . . . . . . . . . . . . . . . 20 |- (b e. Fin -> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> E.f(f:b-->c /\ A.t e. b t C_ (f` t))))
75	74	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) -> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> E.f(f:b-->c /\ A.t e. b t C_ (f` t))))
76		frn 4569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:b-->c -> ran f C_ c)
77	76	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f:b-->c /\ A.t e. b t C_ (f` t)) -> ran f C_ c)
78	77	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> ran f C_ c)
79		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> b e. Fin)
80		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f:b-->c -> f Fn b)
81		dffn4 4623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f Fn b <-> f:b-onto->ran f)
82	80, 81	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (f:b-->c -> f:b-onto->ran f)
83	82	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f:b-->c /\ A.t e. b t C_ (f` t)) -> f:b-onto->ran f)
84	83	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> f:b-onto->ran f)
85		fodomfi 5656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((b e. Fin /\ f:b-onto->ran f) -> ran f ~<_ b)
86	79, 84, 85	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> ran f ~<_ b)
87		domfi 5631	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((b e. Fin /\ ran f ~<_ b) -> ran f e. Fin)
88	79, 86, 87	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> ran f e. Fin)
89	78, 88	jca 310	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (ran f C_ c /\ ran f e. Fin))
90		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (ran f e. (~Pc i^i Fin) <-> (ran f e. ~Pc /\ ran f e. Fin))
91		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- c e. _V
92	91	elpw2 3464	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (ran f e. ~Pc <-> ran f C_ c)
93	92	anbi1i 539	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((ran f e. ~Pc /\ ran f e. Fin) <-> (ran f C_ c /\ ran f e. Fin))
94	90, 93	bitr2i 191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((ran f C_ c /\ ran f e. Fin) <-> ran f e. (~Pc i^i Fin))
95	89, 94	sylib 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> ran f e. (~Pc i^i Fin))
96		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (X = U.b -> (y e. X <-> y e. U.b))
97	96	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. X <-> y e. U.b))
98	1	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. X <-> y e. U.J)
99	97, 98	syl5bbr 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.J <-> y e. U.b))
100		id 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (t = w -> t = w)
101		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (t = w -> (f` t) = (f` w))
102	100, 101	sseq12d 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (t = w -> (t C_ (f` t) <-> w C_ (f` w)))
103	102	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (w e. b -> (A.t e. b t C_ (f` t) -> w C_ (f` w)))
104	103	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ (f:b-->c /\ w e. b)) -> (A.t e. b t C_ (f` t) -> w C_ (f` w)))
105		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (w C_ (f` w) -> (y e. w -> y e. (f` w)))
106		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((y e. (f` w) /\ (f` w) e. ran f) -> y e. U.ran f)
107		fnfvelrn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((f Fn b /\ w e. b) -> (f` w) e. ran f)
108	107, 80	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((f:b-->c /\ w e. b) -> (f` w) e. ran f)
109	106, 108	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((y e. (f` w) /\ (f:b-->c /\ w e. b)) -> y e. U.ran f)
110	109	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((f:b-->c /\ w e. b) -> (y e. (f` w) -> y e. U.ran f))
111	110	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ (f:b-->c /\ w e. b)) -> (y e. (f` w) -> y e. U.ran f))
112	105, 111	syl9r 72	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ (f:b-->c /\ w e. b)) -> (w C_ (f` w) -> (y e. w -> y e. U.ran f)))
113	104, 112	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ (f:b-->c /\ w e. b)) -> (A.t e. b t C_ (f` t) -> (y e. w -> y e. U.ran f)))
114	113	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ f:b-->c) -> (w e. b -> (A.t e. b t C_ (f` t) -> (y e. w -> y e. U.ran f))))
115	114	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ f:b-->c) -> (A.t e. b t C_ (f` t) -> (w e. b -> (y e. w -> y e. U.ran f))))
116	115	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (f:b-->c -> (A.t e. b t C_ (f` t) -> (w e. b -> (y e. w -> y e. U.ran f)))))
117	116	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) -> (f:b-->c -> (A.t e. b t C_ (f` t) -> (w e. b -> (y e. w -> y e. U.ran f)))))
118	117	a1i4 15327	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) -> (f:b-->c -> (A.t e. b t C_ (f` t) -> (X = U.b -> (w e. b -> (y e. w -> y e. U.ran f))))))
119	118	imp44 398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (w e. b -> (y e. w -> y e. U.ran f)))
120	119	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (E.w e. b y e. w -> y e. U.ran f))
121		eluni2 3181	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. U.b <-> E.w e. b y e. w)
122	120, 121	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.b -> y e. U.ran f))
123	99, 122	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.J -> y e. U.ran f))
124		uniss 3199	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (ran f C_ c -> U.ran f C_ U.c)
125	78, 124	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> U.ran f C_ U.c)
126	125	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.ran f -> y e. U.c))
127		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (U.J = U.c -> (y e. U.J <-> y e. U.c))
128	127	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (y e. U.J <-> y e. U.c))
129	128	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.J <-> y e. U.c))
130	126, 129	sylibrd 221	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.ran f -> y e. U.J))
131	123, 130	impbid 574	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> (y e. U.J <-> y e. U.ran f))
132	131	eqrdv 1882	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> U.J = U.ran f)
133		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (d = ran f -> U.d = U.ran f)
134	133	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . 23 |- (d = ran f -> (U.J = U.d <-> U.J = U.ran f))
135	134	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . 22 |- ((ran f e. (~Pc i^i Fin) /\ U.J = U.ran f) -> E.d e. (~Pc i^i Fin)U.J = U.d)
136	95, 132, 135	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) /\ ((f:b-->c /\ A.t e. b t C_ (f` t)) /\ X = U.b)) -> E.d e. (~Pc i^i Fin)U.J = U.d)
137	136	exp32 408	. . . . . . . . . . . . . . . . . . . 20 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) -> ((f:b-->c /\ A.t e. b t C_ (f` t)) -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d)))
138	137	19.23adv 1584	. . . . . . . . . . . . . . . . . . 19 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) -> (E.f(f:b-->c /\ A.t e. b t C_ (f` t)) -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d)))
139	75, 138	syld 30	. . . . . . . . . . . . . . . . . 18 |- (((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) /\ b e. Fin) -> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d)))
140	139	ex 402	. . . . . . . . . . . . . . . . 17 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (b e. Fin -> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d))))
141	140	com23 36	. . . . . . . . . . . . . . . 16 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} -> (b e. Fin -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d))))
142	141	imp3a 388	. . . . . . . . . . . . . . 15 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> ((b C_ {y e. ( fi ` x) | E.z e. c y C_ z} /\ b e. Fin) -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d)))
143		elin 2786	. . . . . . . . . . . . . . . 16 |- (b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin) <-> (b e. ~P{y e. ( fi ` x) | E.z e. c y C_ z} /\ b e. Fin))
144		visset 2295	. . . . . . . . . . . . . . . . . 18 |- b e. _V
145	144	elpw 3037	. . . . . . . . . . . . . . . . 17 |- (b e. ~P{y e. ( fi ` x) | E.z e. c y C_ z} <-> b C_ {y e. ( fi ` x) | E.z e. c y C_ z})
146	145	anbi1i 539	. . . . . . . . . . . . . . . 16 |- ((b e. ~P{y e. ( fi ` x) | E.z e. c y C_ z} /\ b e. Fin) <-> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} /\ b e. Fin))
147	143, 146	bitri 190	. . . . . . . . . . . . . . 15 |- (b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin) <-> (b C_ {y e. ( fi ` x) | E.z e. c y C_ z} /\ b e. Fin))
148	142, 147	syl5ib 223	. . . . . . . . . . . . . 14 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin) -> (X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d)))
149	148	r19.23adv 2215	. . . . . . . . . . . . 13 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (E.b e. (~P{y e. ( fi ` x) | E.z e. c y C_ z} i^i Fin)X = U.b -> E.d e. (~Pc i^i Fin)U.J = U.d))
150	63, 149	syld 30	. . . . . . . . . . . 12 |- ((J = (topGen` ( fi ` x)) /\ c C_ J /\ U.J = U.c) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> E.d e. (~Pc i^i Fin)U.J = U.d))
151	150	3exp 1066	. . . . . . . . . . 11 |- (J = (topGen` ( fi ` x)) -> (c C_ J -> (U.J = U.c -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> E.d e. (~Pc i^i Fin)U.J = U.d))))
152	151	com34 40	. . . . . . . . . 10 |- (J = (topGen` ( fi ` x)) -> (c C_ J -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> (U.J = U.c -> E.d e. (~Pc i^i Fin)U.J = U.d))))
153	152	com23 36	. . . . . . . . 9 |- (J = (topGen` ( fi ` x)) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> (c C_ J -> (U.J = U.c -> E.d e. (~Pc i^i Fin)U.J = U.d))))
154	91	elpw 3037	. . . . . . . . 9 |- (c e. ~PJ <-> c C_ J)
155	153, 154	syl7ib 233	. . . . . . . 8 |- (J = (topGen` ( fi ` x)) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> (c e. ~PJ -> (U.J = U.c -> E.d e. (~Pc i^i Fin)U.J = U.d))))
156	155	r19.21adv 2181	. . . . . . 7 |- (J = (topGen` ( fi ` x)) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> A.c e. ~P J(U.J = U.c -> E.d e. (~Pc i^i Fin)U.J = U.d)))
157		tgcl 8894	. . . . . . . . 9 |- (( fi ` x) e. Bases -> (topGen` ( fi ` x)) e. Top)
158	22, 157	ax-mp 7	. . . . . . . 8 |- (topGen` ( fi ` x)) e. Top
159		eleq1 1957	. . . . . . . 8 |- (J = (topGen` ( fi ` x)) -> (J e. Top <-> (topGen` ( fi ` x)) e. Top))
160	158, 159	mpbiri 211	. . . . . . 7 |- (J = (topGen` ( fi ` x)) -> J e. Top)
161	156, 160	jctild 662	. . . . . 6 |- (J = (topGen` ( fi ` x)) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> (J e. Top /\ A.c e. ~P J(U.J = U.c -> E.d e. (~Pc i^i Fin)U.J = U.d))))
162		iscomp 10330	. . . . . 6 |- (J e. Comp <-> (J e. Top /\ A.c e. ~P J(U.J = U.c -> E.d e. (~Pc i^i Fin)U.J = U.d)))
163	161, 162	syl6ibr 230	. . . . 5 |- (J = (topGen` ( fi ` x)) -> (A.a e. ~P ( fi ` x)(X = U.a -> E.b e. (~Pa i^i Fin)X = U.b) -> J e. Comp))
164	3, 163	syld 30	. . . 4 |- (J = (topGen` ( fi ` x)) -> (A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d) -> J e. Comp))
165	164	imp 377	. . 3 |- ((J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d)) -> J e. Comp)
166	165	19.23aiv 1674	. 2 |- (E.x(J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d)) -> J e. Comp)
167	2, 166	impbii 174	1 |- (J e. Comp <-> E.x(J = (topGen` ( fi ` x)) /\ A.c e. ~P x(X = U.c -> E.d e. (~Pc i^i Fin)X = U.d)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   i^i cin 2592   C_ wss 2593  ~Pcpw 3032  U.cuni 3177   class class class wbr 3338  ran crn 3987   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998   ~<_ cdom 5424  Fincfn 5426  Topctop 8857  Basesctb 8859  topGenctg 8860   fi cfi 10210  Compccomp 10328

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-bases 8863  df-topgen 8864  df-fi 10211  df-comp 10329

Copyright terms: Public domain