Theorem compsub 15431

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology.

Hypothesis

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

Assertion

Ref	Expression
compsub	|- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Comp <-> A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)))

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

Proof of Theorem compsub

Step	Hyp	Ref	Expression
1		stoig3 10253	. . . . 5 |- ((J e. Top /\ S C_ U.J) -> (subSp` <.S, J>.) e. Top)
2		compsub.1	. . . . . 6 |- X = U.J
3	2	sseq2i 2642	. . . . 5 |- (S C_ X <-> S C_ U.J)
4	1, 3	sylan2b 501	. . . 4 |- ((J e. Top /\ S C_ X) -> (subSp` <.S, J>.) e. Top)
5		ibar 705	. . . . 5 |- ((subSp` <.S, J>.) e. Top -> (A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t) <-> ((subSp` <.S, J>.) e. Top /\ A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t))))
6	5	bicomd 580	. . . 4 |- ((subSp` <.S, J>.) e. Top -> (((subSp` <.S, J>.) e. Top /\ A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)) <-> A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
7	4, 6	syl 12	. . 3 |- ((J e. Top /\ S C_ X) -> (((subSp` <.S, J>.) e. Top /\ A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)) <-> A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
8		iscomp 10330	. . 3 |- ((subSp` <.S, J>.) e. Comp <-> ((subSp` <.S, J>.) e. Top /\ A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
9	7, 8	syl5bb 591	. 2 |- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Comp <-> A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
10		unieq 3185	. . . . . . . . . 10 |- (s = {x | E.y e. c x = (y i^i S)} -> U.s = U.{x | E.y e. c x = (y i^i S)})
11	10	eqeq2d 1895	. . . . . . . . 9 |- (s = {x | E.y e. c x = (y i^i S)} -> (U.(subSp` <.S, J>.) = U.s <-> U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)}))
12		pweq 3036	. . . . . . . . . . 11 |- (s = {x | E.y e. c x = (y i^i S)} -> ~Ps = ~P{x | E.y e. c x = (y i^i S)})
13	12	ineq1d 2795	. . . . . . . . . 10 |- (s = {x | E.y e. c x = (y i^i S)} -> (~Ps i^i Fin) = (~P{x | E.y e. c x = (y i^i S)} i^i Fin))
14	13	rexeqdv 2270	. . . . . . . . 9 |- (s = {x | E.y e. c x = (y i^i S)} -> (E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t <-> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t))
15	11, 14	imbi12d 688	. . . . . . . 8 |- (s = {x | E.y e. c x = (y i^i S)} -> ((U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t) <-> (U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t)))
16	15	rcla4va 2378	. . . . . . 7 |- (({x | E.y e. c x = (y i^i S)} e. ~P(subSp` <.S, J>.) /\ A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)) -> (U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t))
17		visset 2295	. . . . . . . . . . . . . . 15 |- c e. _V
18	17	elpw 3037	. . . . . . . . . . . . . 14 |- (c e. ~PJ <-> c C_ J)
19		ssel2 2616	. . . . . . . . . . . . . . . 16 |- ((c C_ J /\ y e. c) -> y e. J)
20		ineq1 2789	. . . . . . . . . . . . . . . . . . 19 |- (d = y -> (d i^i S) = (y i^i S))
21	20	eqeq2d 1895	. . . . . . . . . . . . . . . . . 18 |- (d = y -> (t = (d i^i S) <-> t = (y i^i S)))
22	21	rcla4ev 2381	. . . . . . . . . . . . . . . . 17 |- ((y e. J /\ t = (y i^i S)) -> E.d e. J t = (d i^i S))
23	22	ex 402	. . . . . . . . . . . . . . . 16 |- (y e. J -> (t = (y i^i S) -> E.d e. J t = (d i^i S)))
24	19, 23	syl 12	. . . . . . . . . . . . . . 15 |- ((c C_ J /\ y e. c) -> (t = (y i^i S) -> E.d e. J t = (d i^i S)))
25	24	ex 402	. . . . . . . . . . . . . 14 |- (c C_ J -> (y e. c -> (t = (y i^i S) -> E.d e. J t = (d i^i S))))
26	18, 25	sylbi 216	. . . . . . . . . . . . 13 |- (c e. ~PJ -> (y e. c -> (t = (y i^i S) -> E.d e. J t = (d i^i S))))
27	26	adantl 424	. . . . . . . . . . . 12 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (y e. c -> (t = (y i^i S) -> E.d e. J t = (d i^i S))))
28	27	r19.23adv 2215	. . . . . . . . . . 11 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (E.y e. c t = (y i^i S) -> E.d e. J t = (d i^i S)))
29		simpll 448	. . . . . . . . . . . 12 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> J e. Top)
30		visset 2295	. . . . . . . . . . . . 13 |- t e. _V
31	30	a1i 8	. . . . . . . . . . . 12 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> t e. _V)
32		ssexg 3457	. . . . . . . . . . . . . . . 16 |- ((S C_ U.J /\ U.J e. _V) -> S e. _V)
33		uniexg 3795	. . . . . . . . . . . . . . . 16 |- (J e. Top -> U.J e. _V)
34	32, 33	sylan2 500	. . . . . . . . . . . . . . 15 |- ((S C_ U.J /\ J e. Top) -> S e. _V)
35	34	ancoms 484	. . . . . . . . . . . . . 14 |- ((J e. Top /\ S C_ U.J) -> S e. _V)
36	35, 3	sylan2b 501	. . . . . . . . . . . . 13 |- ((J e. Top /\ S C_ X) -> S e. _V)
37	36	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> S e. _V)
38		issubspt 10247	. . . . . . . . . . . 12 |- ((J e. Top /\ t e. _V /\ S e. _V) -> (t e. (subSp` <.S, J>.) <-> E.d e. J t = (d i^i S)))
39	29, 31, 37, 38	syl111anc 1100	. . . . . . . . . . 11 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (t e. (subSp` <.S, J>.) <-> E.d e. J t = (d i^i S)))
40	28, 39	sylibrd 221	. . . . . . . . . 10 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (E.y e. c t = (y i^i S) -> t e. (subSp` <.S, J>.)))
41		eqeq1 1890	. . . . . . . . . . . 12 |- (x = t -> (x = (y i^i S) <-> t = (y i^i S)))
42	41	rexbidv 2124	. . . . . . . . . . 11 |- (x = t -> (E.y e. c x = (y i^i S) <-> E.y e. c t = (y i^i S)))
43	30, 42	elab 2403	. . . . . . . . . 10 |- (t e. {x | E.y e. c x = (y i^i S)} <-> E.y e. c t = (y i^i S))
44	40, 43	syl5ib 223	. . . . . . . . 9 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (t e. {x | E.y e. c x = (y i^i S)} -> t e. (subSp` <.S, J>.)))
45	44	ssrdv 2622	. . . . . . . 8 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> {x | E.y e. c x = (y i^i S)} C_ (subSp` <.S, J>.))
46	17	abrexex 4836	. . . . . . . . 9 |- {x | E.y e. c x = (y i^i S)} e. _V
47	46	elpw 3037	. . . . . . . 8 |- ({x | E.y e. c x = (y i^i S)} e. ~P(subSp` <.S, J>.) <-> {x | E.y e. c x = (y i^i S)} C_ (subSp` <.S, J>.))
48	45, 47	sylibr 217	. . . . . . 7 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> {x | E.y e. c x = (y i^i S)} e. ~P(subSp` <.S, J>.))
49	16, 48	sylan 497	. . . . . 6 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)) -> (U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t))
50	49	ex 402	. . . . 5 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t) -> (U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t)))
51		stoig2 10252	. . . . . . . . . . . 12 |- ((J e. Top /\ S C_ U.J) -> U.(subSp` <.S, J>.) = S)
52	51, 3	sylan2b 501	. . . . . . . . . . 11 |- ((J e. Top /\ S C_ X) -> U.(subSp` <.S, J>.) = S)
53	52	ad2antrr 440	. . . . . . . . . 10 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U.(subSp` <.S, J>.) = S)
54		visset 2295	. . . . . . . . . . . . . . 15 |- y e. _V
55	54	inex1 3452	. . . . . . . . . . . . . 14 |- (y i^i S) e. _V
56	55	dfiun2 3285	. . . . . . . . . . . . 13 |- U_y e. c (y i^i S) = U.{x | E.y e. c x = (y i^i S)}
57	56	eqcomi 1888	. . . . . . . . . . . 12 |- U.{x | E.y e. c x = (y i^i S)} = U_y e. c (y i^i S)
58	57	a1i 8	. . . . . . . . . . 11 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U.{x | E.y e. c x = (y i^i S)} = U_y e. c (y i^i S))
59		incom 2787	. . . . . . . . . . . . 13 |- (y i^i S) = (S i^i y)
60	59	a1i 8	. . . . . . . . . . . 12 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ y e. c) -> (y i^i S) = (S i^i y))
61	60	iuneq2dv 3279	. . . . . . . . . . 11 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U_y e. c (y i^i S) = U_y e. c (S i^i y))
62		iunin2 3320	. . . . . . . . . . . . 13 |- U_y e. c (S i^i y) = (S i^i U_y e. c y)
63	62	a1i 8	. . . . . . . . . . . 12 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U_y e. c (S i^i y) = (S i^i U_y e. c y))
64		uniiun 3306	. . . . . . . . . . . . . . 15 |- U.c = U_y e. c y
65	64	eqcomi 1888	. . . . . . . . . . . . . 14 |- U_y e. c y = U.c
66	65	a1i 8	. . . . . . . . . . . . 13 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U_y e. c y = U.c)
67	66	ineq2d 2796	. . . . . . . . . . . 12 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> (S i^i U_y e. c y) = (S i^i U.c))
68		sseqin2 2811	. . . . . . . . . . . . . . 15 |- (S C_ U.c <-> (U.c i^i S) = S)
69	68	biimpi 168	. . . . . . . . . . . . . 14 |- (S C_ U.c -> (U.c i^i S) = S)
70		incom 2787	. . . . . . . . . . . . . 14 |- (S i^i U.c) = (U.c i^i S)
71	69, 70	syl5eq 1940	. . . . . . . . . . . . 13 |- (S C_ U.c -> (S i^i U.c) = S)
72	71	adantl 424	. . . . . . . . . . . 12 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> (S i^i U.c) = S)
73	63, 67, 72	3eqtrd 1929	. . . . . . . . . . 11 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U_y e. c (S i^i y) = S)
74	58, 61, 73	3eqtrd 1929	. . . . . . . . . 10 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> U.{x | E.y e. c x = (y i^i S)} = S)
75	53, 74	eqeq12d 1899	. . . . . . . . 9 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> (U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} <-> S = S))
76	53	eqeq1d 1892	. . . . . . . . . 10 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> (U.(subSp` <.S, J>.) = U.t <-> S = U.t))
77	76	rexbidv 2124	. . . . . . . . 9 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> (E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t <-> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)S = U.t))
78	75, 77	imbi12d 688	. . . . . . . 8 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> ((U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t) <-> (S = S -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)S = U.t)))
79		ineq1 2789	. . . . . . . . . . . . . . . 16 |- (y = (f` s) -> (y i^i S) = ((f` s) i^i S))
80	79	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (y = (f` s) -> (s = (y i^i S) <-> s = ((f` s) i^i S)))
81	80	ac6sfi 5509	. . . . . . . . . . . . . 14 |- ((t e. Fin /\ A.s e. t E.y e. c s = (y i^i S)) -> E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)))
82	81	ancoms 484	. . . . . . . . . . . . 13 |- ((A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin) -> E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)))
83	82	adantl 424	. . . . . . . . . . . 12 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) -> E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)))
84		elin 2786	. . . . . . . . . . . . . . . . . . 19 |- (ran f e. (~Pc i^i Fin) <-> (ran f e. ~Pc /\ ran f e. Fin))
85		frn 4569	. . . . . . . . . . . . . . . . . . . . 21 |- (f:t-->c -> ran f C_ c)
86	85	ad2antrl 442	. . . . . . . . . . . . . . . . . . . 20 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> ran f C_ c)
87		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- f e. _V
88	87	rnex 4209	. . . . . . . . . . . . . . . . . . . . 21 |- ran f e. _V
89	88	elpw 3037	. . . . . . . . . . . . . . . . . . . 20 |- (ran f e. ~Pc <-> ran f C_ c)
90	86, 89	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> ran f e. ~Pc)
91		simprr 451	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) -> t e. Fin)
92	91	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> t e. Fin)
93		fodomfi 5656	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((t e. Fin /\ f:t-onto->ran f) -> ran f ~<_ t)
94		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:t-->c -> f Fn t)
95		dffn4 4623	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f Fn t <-> f:t-onto->ran f)
96	94, 95	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:t-->c -> f:t-onto->ran f)
97	93, 96	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((t e. Fin /\ f:t-->c) -> ran f ~<_ t)
98	97	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin) /\ f:t-->c) -> ran f ~<_ t)
99	98	adantll 428	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ f:t-->c) -> ran f ~<_ t)
100	99	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . 20 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> ran f ~<_ t)
101		domfi 5631	. . . . . . . . . . . . . . . . . . . 20 |- ((t e. Fin /\ ran f ~<_ t) -> ran f e. Fin)
102	92, 100, 101	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> ran f e. Fin)
103	84, 90, 102	sylanbrc 527	. . . . . . . . . . . . . . . . . 18 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> ran f e. (~Pc i^i Fin))
104		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (u e. t -> ((u e. t -> u = ((f` u) i^i S)) -> u = ((f` u) i^i S)))
105		inss1 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((f` u) i^i S) C_ (f` u)
106		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (u = ((f` u) i^i S) -> (u C_ (f` u) <-> ((f` u) i^i S) C_ (f` u)))
107	105, 106	mpbiri 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (u = ((f` u) i^i S) -> u C_ (f` u))
108		ssel 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (u C_ (f` u) -> (w e. u -> w e. (f` u)))
109	108	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (u C_ (f` u) -> (w e. u -> (f:t-->c -> w e. (f` u))))
110	107, 109	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u = ((f` u) i^i S) -> (w e. u -> (f:t-->c -> w e. (f` u))))
111	110	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. t -> (u = ((f` u) i^i S) -> (w e. u -> (f:t-->c -> w e. (f` u)))))
112	111	3imp 1061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((u e. t /\ u = ((f` u) i^i S) /\ w e. u) -> (f:t-->c -> w e. (f` u)))
113		fnfvelrn 4786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((f Fn t /\ u e. t) -> (f` u) e. ran f)
114	113	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u e. t -> (f Fn t -> (f` u) e. ran f))
115	114	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((u e. t /\ u = ((f` u) i^i S) /\ w e. u) -> (f Fn t -> (f` u) e. ran f))
116	115, 94	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((u e. t /\ u = ((f` u) i^i S) /\ w e. u) -> (f:t-->c -> (f` u) e. ran f))
117	112, 116	jcad 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((u e. t /\ u = ((f` u) i^i S) /\ w e. u) -> (f:t-->c -> (w e. (f` u) /\ (f` u) e. ran f)))
118	117	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (u e. t -> (u = ((f` u) i^i S) -> (w e. u -> (f:t-->c -> (w e. (f` u) /\ (f` u) e. ran f)))))
119	104, 118	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (u e. t -> ((u e. t -> u = ((f` u) i^i S)) -> (w e. u -> (f:t-->c -> (w e. (f` u) /\ (f` u) e. ran f)))))
120	119	com3r 39	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. u -> (u e. t -> ((u e. t -> u = ((f` u) i^i S)) -> (f:t-->c -> (w e. (f` u) /\ (f` u) e. ran f)))))
121	120	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. u /\ u e. t) -> ((u e. t -> u = ((f` u) i^i S)) -> (f:t-->c -> (w e. (f` u) /\ (f` u) e. ran f))))
122	121	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((u e. t -> u = ((f` u) i^i S)) -> (f:t-->c -> ((w e. u /\ u e. t) -> (w e. (f` u) /\ (f` u) e. ran f))))
123	122	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f:t-->c /\ (u e. t -> u = ((f` u) i^i S))) -> ((w e. u /\ u e. t) -> (w e. (f` u) /\ (f` u) e. ran f)))
124		id 73	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (s = u -> s = u)
125		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (s = u -> (f` s) = (f` u))
126	125	ineq1d 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (s = u -> ((f` s) i^i S) = ((f` u) i^i S))
127	124, 126	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (s = u -> (s = ((f` s) i^i S) <-> u = ((f` u) i^i S)))
128	127	rcla4cv 2377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A.s e. t s = ((f` s) i^i S) -> (u e. t -> u = ((f` u) i^i S)))
129	123, 128	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> ((w e. u /\ u e. t) -> (w e. (f` u) /\ (f` u) e. ran f)))
130		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f` u) e. _V
131		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = (f` u) -> (w e. v <-> w e. (f` u)))
132		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = (f` u) -> (v e. ran f <-> (f` u) e. ran f))
133	131, 132	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = (f` u) -> ((w e. v /\ v e. ran f) <-> (w e. (f` u) /\ (f` u) e. ran f)))
134	130, 133	cla4ev 2371	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((w e. (f` u) /\ (f` u) e. ran f) -> E.v(w e. v /\ v e. ran f))
135	129, 134	syl6 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> ((w e. u /\ u e. t) -> E.v(w e. v /\ v e. ran f)))
136	135	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> (E.u(w e. u /\ u e. t) -> E.v(w e. v /\ v e. ran f)))
137		eluni 3180	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. U.t <-> E.u(w e. u /\ u e. t))
138		eluni 3180	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. U.ran f <-> E.v(w e. v /\ v e. ran f))
139	136, 137, 138	3imtr4g 612	. . . . . . . . . . . . . . . . . . . . 21 |- ((f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> (w e. U.t -> w e. U.ran f))
140	139	ssrdv 2622	. . . . . . . . . . . . . . . . . . . 20 |- ((f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> U.t C_ U.ran f)
141	140	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> U.t C_ U.ran f)
142		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- (S = U.t -> (S C_ U.ran f <-> U.t C_ U.ran f))
143	142	ad2antlr 441	. . . . . . . . . . . . . . . . . . 19 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> (S C_ U.ran f <-> U.t C_ U.ran f))
144	141, 143	mpbird 213	. . . . . . . . . . . . . . . . . 18 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> S C_ U.ran f)
145	103, 144	jca 310	. . . . . . . . . . . . . . . . 17 |- (((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) /\ (f:t-->c /\ A.s e. t s = ((f` s) i^i S))) -> (ran f e. (~Pc i^i Fin) /\ S C_ U.ran f))
146	145	ex 402	. . . . . . . . . . . . . . . 16 |- ((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) -> ((f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> (ran f e. (~Pc i^i Fin) /\ S C_ U.ran f)))
147	146	eximdv 1669	. . . . . . . . . . . . . . 15 |- ((((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) /\ S = U.t) -> (E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> E.f(ran f e. (~Pc i^i Fin) /\ S C_ U.ran f)))
148	147	ex 402	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) -> (S = U.t -> (E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> E.f(ran f e. (~Pc i^i Fin) /\ S C_ U.ran f))))
149	148	com23 36	. . . . . . . . . . . . 13 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) -> (E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> (S = U.t -> E.f(ran f e. (~Pc i^i Fin) /\ S C_ U.ran f))))
150		unieq 3185	. . . . . . . . . . . . . . . 16 |- (d = ran f -> U.d = U.ran f)
151	150	sseq2d 2645	. . . . . . . . . . . . . . 15 |- (d = ran f -> (S C_ U.d <-> S C_ U.ran f))
152	151	rcla4ev 2381	. . . . . . . . . . . . . 14 |- ((ran f e. (~Pc i^i Fin) /\ S C_ U.ran f) -> E.d e. (~Pc i^i Fin)S C_ U.d)
153	152	19.23aiv 1674	. . . . . . . . . . . . 13 |- (E.f(ran f e. (~Pc i^i Fin) /\ S C_ U.ran f) -> E.d e. (~Pc i^i Fin)S C_ U.d)
154	149, 153	syl8 27	. . . . . . . . . . . 12 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) -> (E.f(f:t-->c /\ A.s e. t s = ((f` s) i^i S)) -> (S = U.t -> E.d e. (~Pc i^i Fin)S C_ U.d)))
155	83, 154	mpd 29	. . . . . . . . . . 11 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin)) -> (S = U.t -> E.d e. (~Pc i^i Fin)S C_ U.d))
156		elin 2786	. . . . . . . . . . . 12 |- (t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin) <-> (t e. ~P{x | E.y e. c x = (y i^i S)} /\ t e. Fin))
157	30	elpw 3037	. . . . . . . . . . . . . 14 |- (t e. ~P{x | E.y e. c x = (y i^i S)} <-> t C_ {x | E.y e. c x = (y i^i S)})
158		dfss3 2611	. . . . . . . . . . . . . 14 |- (t C_ {x | E.y e. c x = (y i^i S)} <-> A.s e. t s e. {x | E.y e. c x = (y i^i S)})
159		visset 2295	. . . . . . . . . . . . . . . 16 |- s e. _V
160		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (x = s -> (x = (y i^i S) <-> s = (y i^i S)))
161	160	rexbidv 2124	. . . . . . . . . . . . . . . 16 |- (x = s -> (E.y e. c x = (y i^i S) <-> E.y e. c s = (y i^i S)))
162	159, 161	elab 2403	. . . . . . . . . . . . . . 15 |- (s e. {x | E.y e. c x = (y i^i S)} <-> E.y e. c s = (y i^i S))
163	162	ralbii 2127	. . . . . . . . . . . . . 14 |- (A.s e. t s e. {x | E.y e. c x = (y i^i S)} <-> A.s e. t E.y e. c s = (y i^i S))
164	157, 158, 163	3bitri 194	. . . . . . . . . . . . 13 |- (t e. ~P{x | E.y e. c x = (y i^i S)} <-> A.s e. t E.y e. c s = (y i^i S))
165	164	anbi1i 539	. . . . . . . . . . . 12 |- ((t e. ~P{x | E.y e. c x = (y i^i S)} /\ t e. Fin) <-> (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin))
166	156, 165	bitri 190	. . . . . . . . . . 11 |- (t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin) <-> (A.s e. t E.y e. c s = (y i^i S) /\ t e. Fin))
167	155, 166	sylan2b 501	. . . . . . . . . 10 |- (((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) /\ t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)) -> (S = U.t -> E.d e. (~Pc i^i Fin)S C_ U.d))
168	167	r19.23adva 2216	. . . . . . . . 9 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> (E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)S = U.t -> E.d e. (~Pc i^i Fin)S C_ U.d))
169		eqid 1884	. . . . . . . . . 10 |- S = S
170	169	a1bi 214	. . . . . . . . 9 |- (E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)S = U.t <-> (S = S -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)S = U.t))
171	168, 170	syl5ibr 224	. . . . . . . 8 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> ((S = S -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)S = U.t) -> E.d e. (~Pc i^i Fin)S C_ U.d))
172	78, 171	sylbid 220	. . . . . . 7 |- ((((J e. Top /\ S C_ X) /\ c e. ~PJ) /\ S C_ U.c) -> ((U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t) -> E.d e. (~Pc i^i Fin)S C_ U.d))
173	172	ex 402	. . . . . 6 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (S C_ U.c -> ((U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t) -> E.d e. (~Pc i^i Fin)S C_ U.d)))
174	173	com23 36	. . . . 5 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> ((U.(subSp` <.S, J>.) = U.{x | E.y e. c x = (y i^i S)} -> E.t e. (~P{x | E.y e. c x = (y i^i S)} i^i Fin)U.(subSp` <.S, J>.) = U.t) -> (S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)))
175	50, 174	syld 30	. . . 4 |- (((J e. Top /\ S C_ X) /\ c e. ~PJ) -> (A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t) -> (S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)))
176	175	r19.21adva 2182	. . 3 |- ((J e. Top /\ S C_ X) -> (A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t) -> A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)))
177	2	compsublem 15430	. . 3 |- ((J e. Top /\ S C_ X) -> (A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d) -> A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t)))
178	176, 177	impbid 574	. 2 |- ((J e. Top /\ S C_ X) -> (A.s e. ~P (subSp` <.S, J>.)(U.(subSp` <.S, J>.) = U.s -> E.t e. (~Ps i^i Fin)U.(subSp` <.S, J>.) = U.t) <-> A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)))
179	9, 178	bitrd 587	1 |- ((J e. Top /\ S C_ X) -> ((subSp` <.S, J>.) e. Comp <-> A.c e. ~P J(S C_ U.c -> E.d e. (~Pc i^i Fin)S C_ U.d)))

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

This theorem is referenced by:  cptclsscpt 15432  uncomp 15433  hscptsscld 15434

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-reg 5695

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-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-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-opr 4886  df-oprab 4887  df-1o 5177  df-er 5318  df-en 5427  df-dom 5428  df-fin 5430  df-top 8861  df-topsp 8862  df-subsp 10243  df-comp 10329

Copyright terms: Public domain