reheibor - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
GIF version

Theorem reheibor 12081

Description: Heine-Borel theorem for real numbers. A subset of ℝ is compact iff it is closed and bounded.

**Hypotheses**
Ref	Expression
reheibor.1	⊢ R = ((abs ∘ − ) ↾ (ℝ × ℝ))
reheibor.2	⊢ M = (R ↾ (Y × Y))
reheibor.3	⊢ T = (Open ‘M)
reheibor.4	⊢ U = (Open ‘R)

**Assertion**
Ref	Expression
reheibor	⊢ (Y ⊆ ℝ → (T ∈ Comp ↔ (Y ∈ (Clsd ‘U) ⋀ M ∈ Bnd)))

**Proof of Theorem reheibor**
Step	Hyp	Ref	Expression
1		eqid 1518	. . . 4 ⊢ (ℝ ↑_m (1...1)) = (ℝ ↑_m (1...1))
2		eqid 1518	. . . 4 ⊢ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) = ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))
3		eqid 1518	. . . 4 ⊢ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) = (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))
4		eqid 1518	. . . 4 ⊢ (Open ‘(Rn ‘1)) = (Open ‘(Rn ‘1))
5	1, 2, 3, 4	rrnheibor 12079	. . 3 ⊢ ((1 ∈ ℕ ⋀ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ⊆ (ℝ ↑_m (1...1))) → ((Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Comp ↔ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ∈ (Clsd ‘(Open ‘(Rn ‘1))) ⋀ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Bnd)))
6		1nn 6079	. . 3 ⊢ 1 ∈ ℕ
7		imassrn 3507	. . . . 5 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ⊆ ran {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))}
8		eqid 1518	. . . . . . 7 ⊢ {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} = {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))}
9		fss 3742	. . . . . . . . . 10 ⊢ ((({1} × {x}):{1}–→{x} ⋀ {x} ⊆ ℝ) → ({1} × {x}):{1}–→ℝ)
10		fconstg 3766	. . . . . . . . . 10 ⊢ (x ∈ ℝ → ({1} × {x}):{1}–→{x})
11		snssi 2530	. . . . . . . . . 10 ⊢ (x ∈ ℝ → {x} ⊆ ℝ)
12	9, 10, 11	sylanc 473	. . . . . . . . 9 ⊢ (x ∈ ℝ → ({1} × {x}):{1}–→ℝ)
13		reex 5466	. . . . . . . . . 10 ⊢ ℝ ∈ V
14		snex 2826	. . . . . . . . . 10 ⊢ {1} ∈ V
15	13, 14	elmap 4475	. . . . . . . . 9 ⊢ (({1} × {x}) ∈ (ℝ ↑_m {1}) ↔ ({1} × {x}):{1}–→ℝ)
16	12, 15	sylibr 198	. . . . . . . 8 ⊢ (x ∈ ℝ → ({1} × {x}) ∈ (ℝ ↑_m {1}))
17		1z 6327	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
18		fzsn 11865	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (1...1) = {1})
19	17, 18	ax-mp 7	. . . . . . . . 9 ⊢ (1...1) = {1}
20	19	opreq2i 4030	. . . . . . . 8 ⊢ (ℝ ↑_m (1...1)) = (ℝ ↑_m {1})
21	16, 20	syl6eleqr 1602	. . . . . . 7 ⊢ (x ∈ ℝ → ({1} × {x}) ∈ (ℝ ↑_m (1...1)))
22	8, 21	fopab 3941	. . . . . 6 ⊢ {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))}:ℝ–→(ℝ ↑_m (1...1))
23		frn 3740	. . . . . 6 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))}:ℝ–→(ℝ ↑_m (1...1)) → ran {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ⊆ (ℝ ↑_m (1...1)))
24	22, 23	ax-mp 7	. . . . 5 ⊢ ran {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ⊆ (ℝ ↑_m (1...1))
25	7, 24	sstri 2125	. . . 4 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ⊆ (ℝ ↑_m (1...1))
26	25	a1i 8	. . 3 ⊢ (Y ⊆ ℝ → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ⊆ (ℝ ↑_m (1...1)))
27	5, 6, 26	sylancr 474	. 2 ⊢ (Y ⊆ ℝ → ((Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Comp ↔ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ∈ (Clsd ‘(Open ‘(Rn ‘1))) ⋀ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Bnd)))
28		hmph 11030	. . . . . 6 ⊢ ((T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top) → (T ~= (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ↔ ∃f f ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))))
29	13	opabex2 3716	. . . . . . . 8 ⊢ {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ V
30		resexg 3484	. . . . . . . 8 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ V → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ V)
31	29, 30	ax-mp 7	. . . . . . 7 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ V
32		eleq1 1577	. . . . . . 7 ⊢ (f = ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) → (f ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))) ↔ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))))
33	31, 32	cla4ev 1915	. . . . . 6 ⊢ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))) → ∃f f ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))))
34	28, 33	syl5bir 208	. . . . 5 ⊢ ((T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top) → (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))) → T ~= (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))))
35	34	imp 348	. . . 4 ⊢ (((T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top) ⋀ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))) → T ~= (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))
36		comptoppr 11495	. . . . 5 ⊢ ((T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top ⋀ T ~= (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))) → (T ∈ Comp ↔ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Comp))
37	36	3expa 839	. . . 4 ⊢ (((T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top) ⋀ T ~= (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))) → (T ∈ Comp ↔ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Comp))
38	35, 37	syldan 469	. . 3 ⊢ (((T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top) ⋀ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))) → (T ∈ Comp ↔ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Comp))
39		reheibor.2	. . . . . 6 ⊢ M = (R ↾ (Y × Y))
40		reheibor.1	. . . . . . . 8 ⊢ R = ((abs ∘ − ) ↾ (ℝ × ℝ))
41	40	remet 8121	. . . . . . 7 ⊢ R ∈ Met
42		metres 8033	. . . . . . 7 ⊢ (R ∈ Met → (R ↾ (Y × Y)) ∈ Met)
43	41, 42	ax-mp 7	. . . . . 6 ⊢ (R ↾ (Y × Y)) ∈ Met
44	39, 43	eqeltri 1587	. . . . 5 ⊢ M ∈ Met
45		reheibor.3	. . . . . 6 ⊢ T = (Open ‘M)
46	45	opntop 8080	. . . . 5 ⊢ (M ∈ Met → T ∈ Top)
47	44, 46	ax-mp 7	. . . 4 ⊢ T ∈ Top
48		rrnmet 12072	. . . . . . 7 ⊢ (1 ∈ ℕ → (Rn ‘1) ∈ Met)
49	6, 48	ax-mp 7	. . . . . 6 ⊢ (Rn ‘1) ∈ Met
50		metres 8033	. . . . . 6 ⊢ ((Rn ‘1) ∈ Met → ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Met)
51	49, 50	ax-mp 7	. . . . 5 ⊢ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Met
52	3	opntop 8080	. . . . 5 ⊢ (((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Met → (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top)
53	51, 52	ax-mp 7	. . . 4 ⊢ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top
54	47, 53	pm3.2i 283	. . 3 ⊢ (T ∈ Top ⋀ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Top)
55	40	remetba 8120	. . . . . 6 ⊢ ℝ = dom dom R
56		eqid 1518	. . . . . 6 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) = ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)
57	55, 56, 39, 2	ismtyres 12010	. . . . 5 ⊢ (((R ∈ Met ⋀ (Rn ‘1) ∈ Met) ⋀ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (RIsmty(Rn ‘1)) ⋀ Y ⊆ ℝ)) → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (MIsmty((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))
58	41	a1i 8	. . . . 5 ⊢ (Y ⊆ ℝ → R ∈ Met)
59	49	a1i 8	. . . . 5 ⊢ (Y ⊆ ℝ → (Rn ‘1) ∈ Met)
60	40, 8	ismrer1 12080	. . . . . 6 ⊢ {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (RIsmty(Rn ‘1))
61	60	a1i 8	. . . . 5 ⊢ (Y ⊆ ℝ → {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (RIsmty(Rn ‘1)))
62		id 59	. . . . 5 ⊢ (Y ⊆ ℝ → Y ⊆ ℝ)
63	57, 58, 59, 61, 62	syl2anc 475	. . . 4 ⊢ (Y ⊆ ℝ → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (MIsmty((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))
64	45, 3	ismtyhmeo 12007	. . . . 5 ⊢ ((M ∈ Met ⋀ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Met) → (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (MIsmty((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))))))
65	44, 51, 64	mp2an 701	. . . 4 ⊢ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (MIsmty((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))))
66	63, 65	syl 10	. . 3 ⊢ (Y ⊆ ℝ → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (T Homeo (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))))
67	38, 54, 66	sylancr 474	. 2 ⊢ (Y ⊆ ℝ → (T ∈ Comp ↔ (Open ‘((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y)))) ∈ Comp))
68		reheibor.4	. . . . . . . 8 ⊢ U = (Open ‘R)
69	55, 68	uniopn2 8071	. . . . . . 7 ⊢ (R ∈ Met → ∪U = ℝ)
70	41, 69	ax-mp 7	. . . . . 6 ⊢ ∪U = ℝ
71	70	eqcomi 1522	. . . . 5 ⊢ ℝ = ∪U
72	71	hmeocld 11961	. . . 4 ⊢ (((U ∈ Top ⋀ (Open ‘(Rn ‘1)) ∈ Top) ⋀ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (U Homeo (Open ‘(Rn ‘1))) ⋀ Y ⊆ ℝ)) → (Y ∈ (Clsd ‘U) ↔ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ∈ (Clsd ‘(Open ‘(Rn ‘1)))))
73	68	opntop 8080	. . . . . 6 ⊢ (R ∈ Met → U ∈ Top)
74	41, 73	ax-mp 7	. . . . 5 ⊢ U ∈ Top
75	74	a1i 8	. . . 4 ⊢ (Y ⊆ ℝ → U ∈ Top)
76	4	opntop 8080	. . . . . 6 ⊢ ((Rn ‘1) ∈ Met → (Open ‘(Rn ‘1)) ∈ Top)
77	49, 76	ax-mp 7	. . . . 5 ⊢ (Open ‘(Rn ‘1)) ∈ Top
78	77	a1i 8	. . . 4 ⊢ (Y ⊆ ℝ → (Open ‘(Rn ‘1)) ∈ Top)
79	68, 4	ismtyhmeo 12007	. . . . . . 7 ⊢ ((R ∈ Met ⋀ (Rn ‘1) ∈ Met) → ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (RIsmty(Rn ‘1)) → {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (U Homeo (Open ‘(Rn ‘1)))))
80	41, 49, 79	mp2an 701	. . . . . 6 ⊢ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (RIsmty(Rn ‘1)) → {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (U Homeo (Open ‘(Rn ‘1))))
81	60, 80	ax-mp 7	. . . . 5 ⊢ {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (U Homeo (Open ‘(Rn ‘1)))
82	81	a1i 8	. . . 4 ⊢ (Y ⊆ ℝ → {x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ∈ (U Homeo (Open ‘(Rn ‘1))))
83	72, 75, 78, 82, 62	syl2anc 475	. . 3 ⊢ (Y ⊆ ℝ → (Y ∈ (Clsd ‘U) ↔ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ∈ (Clsd ‘(Open ‘(Rn ‘1)))))
84		ismtybnd 12009	. . . 4 ⊢ ((M ∈ Met ⋀ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Met ⋀ ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} ↾ Y) ∈ (MIsmty((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))))) → (M ∈ Bnd ↔ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Bnd))
85	44	a1i 8	. . . 4 ⊢ (Y ⊆ ℝ → M ∈ Met)
86	51	a1i 8	. . . 4 ⊢ (Y ⊆ ℝ → ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Met)
87	84, 85, 86, 63	syl3anc 864	. . 3 ⊢ (Y ⊆ ℝ → (M ∈ Bnd ↔ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Bnd))
88	83, 87	anbi12d 631	. 2 ⊢ (Y ⊆ ℝ → ((Y ∈ (Clsd ‘U) ⋀ M ∈ Bnd) ↔ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) ∈ (Clsd ‘(Open ‘(Rn ‘1))) ⋀ ((Rn ‘1) ↾ (({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y) × ({x, y∣(x ∈ ℝ ⋀ y = ({1} × {x}))} “ Y))) ∈ Bnd)))
89	27, 67, 88	3bitr4d 553	1 ⊢ (Y ⊆ ℝ → (T ∈ Comp ↔ (Y ∈ (Clsd ‘U) ⋀ M ∈ Bnd)))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 144 ⋀ wa 221 = wceq 992 ∈ wcel 994 ∃wex 1016 Vcvv 1857 ⊆ wss 2099 {csn 2467 ∪cuni 2569 class class class wbr 2692 {copab 2740 × cxp 3249 ran crn 3252 ↾ cres 3253 “ cima 3254 ∘ ccom 3255 –→wf 3259 ‘cfv 3263 (class class class)co 4021 ↑_m cm 4463 ℝcr 5387 1c1 5389 − cmin 5446 ℕcn 5450 ℤcz 5452 ...cfz 6595 abscabs 6951 Topctop 7800 Clsdccld 7870 Metcme 7999 Opencopn 8002 Homeo chomeosm 11019 ~= chomeo 11020 Compccomp 11112 Bndcbnd 11987 Ismtycismty 12001 Rncrrn 12067

This theorem is referenced by: icccmp 12083

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-9 1001 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-rep 2767 ax-sep 2777 ax-nul 2784 ax-pow 2818 ax-pr 2855 ax-un 3089 ax-reg 4736 ax-inf2 4770 ax-ac 4890

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-nel 1631 df-ral 1695 df-rex 1696 df-reu 1697 df-rab 1698 df-v 1858 df-sbc 1987 df-csb 2052 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-pss 2107 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-tp 2473 df-op 2474 df-uni 2570 df-int 2601 df-iun 2635 df-iin 2636 df-br 2693 df-opab 2741 df-tr 2755 df-eprel 2910 df-id 2913 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-on 2979 df-lim 2980 df-suc 2981 df-om 3219 df-xp 3265 df-rel 3266 df-cnv 3267 df-co 3268 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fun 3273 df-fn 3274 df-f 3275 df-f1 3276 df-fo 3277 df-f1o 3278 df-fv 3279 df-iso 3280 df-opr 4023 df-oprab 4024 df-1st 4140 df-2nd 4141 df-rdg 4233 df-1o 4269 df-2o 4270 df-oadd 4271 df-omul 4272 df-er 4401 df-ec 4403 df-qs 4406 df-map 4465 df-en 4509 df-dom 4510 df-sdom 4511 df-fin 4512 df-sup 4717 df-r1 4789 df-rank 4790 df-card 4962 df-ni 5154 df-pli 5155 df-mi 5156 df-lti 5157 df-plpq 5189 df-mpq 5190 df-enq 5191 df-nq 5192 df-plq 5193 df-mq 5194 df-rq 5195 df-ltq 5196 df-1q 5197 df-np 5240 df-1p 5241 df-plp 5242 df-mp 5243 df-ltp 5244 df-plpr 5318 df-mpr 5319 df-enr 5320 df-nr 5321 df-plr 5322 df-mr 5323 df-ltr 5324 df-0r 5325 df-1r 5326 df-m1r 5327 df-c 5394 df-0 5395 df-1 5396 df-i 5397 df-r 5398 df-plus 5399 df-mul 5400 df-lt 5401 df-sub 5510 df-neg 5512 df-pnf 5641 df-mnf 5642 df-xr 5643 df-ltxr 5644 df-le 5645 df-div 5855 df-n 6070 df-2 6116 df-3 6117 df-4 6118 df-rp 6191 df-n0 6268 df-z 6304 df-fl 6422 df-uz 6545 df-fz 6596 df-seq1 6673 df-shft 6706 df-seqz 6728 df-seq0 6729 df-exp 6764 df-sqr 6871 df-re 6952 df-im 6953 df-cj 6954 df-abs 6955 df-clim 7178 df-sum 7183 df-top 7804 df-cld 7873 df-ntr 7874 df-cls 7875 df-nei 7923 df-lp 7951 df-cn 7964 df-met 8003 df-bl 8005 df-opn 8006 df-lm 8133 df-cau 8134 df-cmet 8135 df-homeo 11021 df-hmph 11029 df-comp 11113 df-totbnd 11988 df-bnd 11994 df-ismty 12002 df-rrn 12068