Theorem reheibor

Description: Heine-Borel theorem for real numbers. A subset of RR is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	reheibor.2	|- M = ( ( abs o. - ) |` ( Y X. Y ) )
	reheibor.3	|- T = ( MetOpen ` M )
	reheibor.4	|- U = ( topGen ` ran (,) )
Assertion	reheibor	|- ( Y C_ RR -> ( T e. Comp <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		reheibor.2	|- M = ( ( abs o. - ) |` ( Y X. Y ) )
2		reheibor.3	|- T = ( MetOpen ` M )
3		reheibor.4	|- U = ( topGen ` ran (,) )
4		df1o2	|- 1o = { (/) }
5		snfi	|- { (/) } e. Fin
6	4 5	eqeltri	|- 1o e. Fin
7		imassrn	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) C_ ran ( x e. RR |-> ( { (/) } X. { x } ) )
8		0ex	|- (/) e. _V
9		eqid	|- ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
10		eqid	|- ( x e. RR |-> ( { (/) } X. { x } ) ) = ( x e. RR |-> ( { (/) } X. { x } ) )
11	9 10	ismrer1	|- ( (/) e. _V -> ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` { (/) } ) ) )
12	8 11	ax-mp	|- ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` { (/) } ) )
13	4	fveq2i	|- ( Rn ` 1o ) = ( Rn ` { (/) } )
14	13	oveq2i	|- ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) = ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` { (/) } ) )
15	12 14	eleqtrri	|- ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) )
16	9	rexmet	|- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
17		eqid	|- ( RR ^m 1o ) = ( RR ^m 1o )
18	17	rrnmet	|- ( 1o e. Fin -> ( Rn ` 1o ) e. ( Met ` ( RR ^m 1o ) ) )
19		metxmet	|- ( ( Rn ` 1o ) e. ( Met ` ( RR ^m 1o ) ) -> ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) ) )
20	6 18 19	mp2b	|- ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) )
21		isismty	|- ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) ) ) -> ( ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) <-> ( ( x e. RR |-> ( { (/) } X. { x } ) ) : RR -1-1-onto-> ( RR ^m 1o ) /\ A. y e. RR A. z e. RR ( y ( ( abs o. - ) |` ( RR X. RR ) ) z ) = ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) ` y ) ( Rn ` 1o ) ( ( x e. RR |-> ( { (/) } X. { x } ) ) ` z ) ) ) ) )
22	16 20 21	mp2an	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) <-> ( ( x e. RR |-> ( { (/) } X. { x } ) ) : RR -1-1-onto-> ( RR ^m 1o ) /\ A. y e. RR A. z e. RR ( y ( ( abs o. - ) |` ( RR X. RR ) ) z ) = ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) ` y ) ( Rn ` 1o ) ( ( x e. RR |-> ( { (/) } X. { x } ) ) ` z ) ) ) )
23	15 22	mpbi	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) : RR -1-1-onto-> ( RR ^m 1o ) /\ A. y e. RR A. z e. RR ( y ( ( abs o. - ) |` ( RR X. RR ) ) z ) = ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) ` y ) ( Rn ` 1o ) ( ( x e. RR |-> ( { (/) } X. { x } ) ) ` z ) ) )
24	23	simpli	|- ( x e. RR |-> ( { (/) } X. { x } ) ) : RR -1-1-onto-> ( RR ^m 1o )
25		f1of	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) : RR -1-1-onto-> ( RR ^m 1o ) -> ( x e. RR |-> ( { (/) } X. { x } ) ) : RR --> ( RR ^m 1o ) )
26		frn	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) : RR --> ( RR ^m 1o ) -> ran ( x e. RR |-> ( { (/) } X. { x } ) ) C_ ( RR ^m 1o ) )
27	24 25 26	mp2b	|- ran ( x e. RR |-> ( { (/) } X. { x } ) ) C_ ( RR ^m 1o )
28	7 27	sstri	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) C_ ( RR ^m 1o )
29	28	a1i	|- ( Y C_ RR -> ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) C_ ( RR ^m 1o ) )
30		eqid	|- ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) = ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) )
31		eqid	|- ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) = ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) )
32		eqid	|- ( MetOpen ` ( Rn ` 1o ) ) = ( MetOpen ` ( Rn ` 1o ) )
33	17 30 31 32	rrnheibor	|- ( ( 1o e. Fin /\ ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) C_ ( RR ^m 1o ) ) -> ( ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp <-> ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) e. ( Clsd ` ( MetOpen ` ( Rn ` 1o ) ) ) /\ ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( Bnd ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
34	6 29 33	sylancr	|- ( Y C_ RR -> ( ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp <-> ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) e. ( Clsd ` ( MetOpen ` ( Rn ` 1o ) ) ) /\ ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( Bnd ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
35		cnxmet	|- ( abs o. - ) e. ( *Met ` CC )
36		id	|- ( Y C_ RR -> Y C_ RR )
37		ax-resscn	|- RR C_ CC
38	36 37	sstrdi	|- ( Y C_ RR -> Y C_ CC )
39		xmetres2	|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ Y C_ CC ) -> ( ( abs o. - ) |` ( Y X. Y ) ) e. ( *Met ` Y ) )
40	35 38 39	sylancr	|- ( Y C_ RR -> ( ( abs o. - ) |` ( Y X. Y ) ) e. ( *Met ` Y ) )
41	1 40	eqeltrid	|- ( Y C_ RR -> M e. ( *Met ` Y ) )
42		xmetres2	|- ( ( ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) ) /\ ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) C_ ( RR ^m 1o ) ) -> ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( *Met ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) )
43	20 29 42	sylancr	|- ( Y C_ RR -> ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( *Met ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) )
44	2 31	ismtyhmeo	|- ( ( M e. ( *Met ` Y ) /\ ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( *Met ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) -> ( M Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) C_ ( T Homeo ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ) )
45	41 43 44	syl2anc	|- ( Y C_ RR -> ( M Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) C_ ( T Homeo ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ) )
46	16	a1i	|- ( Y C_ RR -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) )
47	20	a1i	|- ( Y C_ RR -> ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) ) )
48	15	a1i	|- ( Y C_ RR -> ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) )
49		eqid	|- ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) = ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y )
50		eqid	|- ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) ) = ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) )
51	49 50 30	ismtyres	|- ( ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) ) ) /\ ( ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) /\ Y C_ RR ) ) -> ( ( x e. RR |-> ( { (/) } X. { x } ) ) |` Y ) e. ( ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) ) Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
52	46 47 48 36 51	syl22anc	|- ( Y C_ RR -> ( ( x e. RR |-> ( { (/) } X. { x } ) ) |` Y ) e. ( ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) ) Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
53		xpss12	|- ( ( Y C_ RR /\ Y C_ RR ) -> ( Y X. Y ) C_ ( RR X. RR ) )
54	53	anidms	|- ( Y C_ RR -> ( Y X. Y ) C_ ( RR X. RR ) )
55	54	resabs1d	|- ( Y C_ RR -> ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) ) = ( ( abs o. - ) |` ( Y X. Y ) ) )
56	55 1	eqtr4di	|- ( Y C_ RR -> ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) ) = M )
57	56	oveq1d	|- ( Y C_ RR -> ( ( ( ( abs o. - ) |` ( RR X. RR ) ) |` ( Y X. Y ) ) Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) = ( M Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
58	52 57	eleqtrd	|- ( Y C_ RR -> ( ( x e. RR |-> ( { (/) } X. { x } ) ) |` Y ) e. ( M Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
59	45 58	sseldd	|- ( Y C_ RR -> ( ( x e. RR |-> ( { (/) } X. { x } ) ) |` Y ) e. ( T Homeo ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ) )
60		hmphi	|- ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) |` Y ) e. ( T Homeo ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ) -> T ~= ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
61	59 60	syl	|- ( Y C_ RR -> T ~= ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
62		cmphmph	|- ( T ~= ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) -> ( T e. Comp -> ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp ) )
63		hmphsym	|- ( T ~= ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) -> ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ~= T )
64		cmphmph	|- ( ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ~= T -> ( ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp -> T e. Comp ) )
65	63 64	syl	|- ( T ~= ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) -> ( ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp -> T e. Comp ) )
66	62 65	impbid	|- ( T ~= ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) -> ( T e. Comp <-> ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp ) )
67	61 66	syl	|- ( Y C_ RR -> ( T e. Comp <-> ( MetOpen ` ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) e. Comp ) )
68		eqid	|- ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
69	9 68	tgioo	|- ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
70	3 69	eqtri	|- U = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
71	70 32	ismtyhmeo	|- ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( Rn ` 1o ) e. ( *Met ` ( RR ^m 1o ) ) ) -> ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) C_ ( U Homeo ( MetOpen ` ( Rn ` 1o ) ) ) )
72	16 20 71	mp2an	|- ( ( ( abs o. - ) |` ( RR X. RR ) ) Ismty ( Rn ` 1o ) ) C_ ( U Homeo ( MetOpen ` ( Rn ` 1o ) ) )
73	72 15	sselii	|- ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( U Homeo ( MetOpen ` ( Rn ` 1o ) ) )
74		retopon	|- ( topGen ` ran (,) ) e. ( TopOn ` RR )
75	3 74	eqeltri	|- U e. ( TopOn ` RR )
76	75	toponunii	|- RR = U. U
77	76	hmeocld	|- ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) e. ( U Homeo ( MetOpen ` ( Rn ` 1o ) ) ) /\ Y C_ RR ) -> ( Y e. ( Clsd ` U ) <-> ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) e. ( Clsd ` ( MetOpen ` ( Rn ` 1o ) ) ) ) )
78	73 36 77	sylancr	|- ( Y C_ RR -> ( Y e. ( Clsd ` U ) <-> ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) e. ( Clsd ` ( MetOpen ` ( Rn ` 1o ) ) ) ) )
79		ismtybnd	|- ( ( M e. ( *Met ` Y ) /\ ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( *Met ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) /\ ( ( x e. RR |-> ( { (/) } X. { x } ) ) |` Y ) e. ( M Ismty ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) ) -> ( M e. ( Bnd ` Y ) <-> ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( Bnd ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) )
80	41 43 58 79	syl3anc	|- ( Y C_ RR -> ( M e. ( Bnd ` Y ) <-> ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( Bnd ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) )
81	78 80	anbi12d	|- ( Y C_ RR -> ( ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) <-> ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) e. ( Clsd ` ( MetOpen ` ( Rn ` 1o ) ) ) /\ ( ( Rn ` 1o ) |` ( ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) X. ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) e. ( Bnd ` ( ( x e. RR |-> ( { (/) } X. { x } ) ) " Y ) ) ) ) )
82	34 67 81	3bitr4d	|- ( Y C_ RR -> ( T e. Comp <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )