xrsmopn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xrsmopn		Structured version Visualization version GIF version

Theorem xrsmopn 24757

Description: The metric on the extended reals generates a topology, but this does not match the order topology on ℝ^*; for example {+∞} is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.)

**Hypotheses**
Ref	Expression
xrsxmet.1	⊢ 𝐷 = (dist‘ℝ^*_𝑠)
xrsmopn.1	⊢ 𝐽 = (MetOpen‘𝐷)

**Assertion**
Ref	Expression
xrsmopn	⊢ (ordTop‘ ≤ ) ⊆ 𝐽

Proof of Theorem xrsmopn Dummy variables 𝑥 𝑟 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elssuni 4894	. . . 4 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ⊆ ∪ (ordTop‘ ≤ ))
2		letopuni 23151	. . . 4 ⊢ ℝ^* = ∪ (ordTop‘ ≤ )
3	1, 2	sseqtrrdi 3975	. . 3 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ⊆ ℝ^*)
4		eqid 2736	. . . . . . . 8 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
5	4	rexmet 24735	. . . . . . 7 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
6		letop 23150	. . . . . . . . 9 ⊢ (ordTop‘ ≤ ) ∈ Top
7		reex 11117	. . . . . . . . 9 ⊢ ℝ ∈ V
8		elrestr 17348	. . . . . . . . 9 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ (ordTop‘ ≤ )) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
9	6, 7, 8	mp3an12 1453	. . . . . . . 8 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
10	9	ad2antrr 726	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
11		elin 3917	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑥 ∩ ℝ) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ))
12	11	biimpri 228	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ))
13	12	adantll 714	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ))
14		eqid 2736	. . . . . . . . . 10 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = ((ordTop‘ ≤ ) ↾_t ℝ)
15	14	xrtgioo 24751	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾_t ℝ)
16		eqid 2736	. . . . . . . . . 10 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
17	4, 16	tgioo 24740	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
18	15, 17	eqtr3i 2761	. . . . . . . 8 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
19	18	mopni2 24437	. . . . . . 7 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ) ∧ 𝑦 ∈ (𝑥 ∩ ℝ)) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ))
20	5, 10, 13, 19	mp3an2i 1468	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ))
21		xrsxmet.1	. . . . . . . . . . . 12 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
22	21	xrsxmet 24754	. . . . . . . . . . 11 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)
23		simplr 768	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ ℝ)
24		ressxr 11176	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℝ^*
25		sseqin2 4175	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℝ^* ↔ (ℝ^* ∩ ℝ) = ℝ)
26	24, 25	mpbi 230	. . . . . . . . . . . 12 ⊢ (ℝ^* ∩ ℝ) = ℝ
27	23, 26	eleqtrrdi 2847	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ (ℝ^* ∩ ℝ))
28		rpxr 12915	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
29	28	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ^*)
30	21	xrsdsre 24755	. . . . . . . . . . . . 13 ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	eqcomi 2745	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = (𝐷 ↾ (ℝ × ℝ))
32	31	blres 24375	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ (ℝ^ ∩ ℝ) ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ))
33	22, 27, 29, 32	mp3an2i 1468	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ))
34	21	xrsblre 24756	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
35	28, 34	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
36	35	adantll 714	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
37		dfss2 3919	. . . . . . . . . . 11 ⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ ℝ ↔ ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟))
38	36, 37	sylib 218	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟))
39	33, 38	eqtrd 2771	. . . . . . . . 9 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (𝑦(ball‘𝐷)𝑟))
40	39	sseq1d 3965	. . . . . . . 8 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) ↔ (𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ)))
41		inss1 4189	. . . . . . . . 9 ⊢ (𝑥 ∩ ℝ) ⊆ 𝑥
42		sstr 3942	. . . . . . . . 9 ⊢ (((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) ∧ (𝑥 ∩ ℝ) ⊆ 𝑥) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
43	41, 42	mpan2 691	. . . . . . . 8 ⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
44	40, 43	biimtrdi 253	. . . . . . 7 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
45	44	reximdva 3149	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
46	20, 45	mpd 15	. . . . 5 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
47		1rp 12909	. . . . . 6 ⊢ 1 ∈ ℝ⁺
48	3	sselda 3933	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℝ^*)
49	48	adantr 480	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ^*)
50		rpxr 12915	. . . . . . . . . 10 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
51	47, 50	mp1i 13	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 1 ∈ ℝ^*)
52		elbl 24332	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 1 ∈ ℝ^) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ^ ∧ (𝑦𝐷𝑧) < 1)))
53	22, 49, 51, 52	mp3an2i 1468	. . . . . . . 8 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)))
54		simp2 1137	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → ¬ 𝑦 ∈ ℝ)
55	48	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ ℝ^*)
56	55	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ^*)
57		simpl3l 1229	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ ℝ^*)
58		xmetcl 24275	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 𝑧 ∈ ℝ^) → (𝑦𝐷𝑧) ∈ ℝ^)
59	22, 56, 57, 58	mp3an2i 1468	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ^*)
60		1red 11133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 1 ∈ ℝ)
61		xmetge0 24288	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 𝑧 ∈ ℝ^*) → 0 ≤ (𝑦𝐷𝑧))
62	22, 56, 57, 61	mp3an2i 1468	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 0 ≤ (𝑦𝐷𝑧))
63		simpl3r 1230	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) < 1)
64		1xr 11191	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ^*
65		xrltle 13063	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦𝐷𝑧) ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1))
66	59, 64, 65	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1))
67	63, 66	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ≤ 1)
68		xrrege0 13089	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦𝐷𝑧) ∈ ℝ^* ∧ 1 ∈ ℝ) ∧ (0 ≤ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≤ 1)) → (𝑦𝐷𝑧) ∈ ℝ)
69	59, 60, 62, 67, 68	syl22anc 838	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ)
70		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧)
71	21	xrsdsreclb 21368	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
72	56, 57, 70, 71	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
73	69, 72	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
74	73	simpld 494	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ)
75	74	ex 412	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ))
76	75	necon1bd 2950	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧))
77		simp1r 1199	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ 𝑥)
78		elequ1 2120	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
79	77, 78	syl5ibcom 245	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 = 𝑧 → 𝑧 ∈ 𝑥))
80	76, 79	syld 47	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥))
81	54, 80	mpd 15	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑧 ∈ 𝑥)
82	81	3expia 1121	. . . . . . . 8 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1) → 𝑧 ∈ 𝑥))
83	53, 82	sylbid 240	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) → 𝑧 ∈ 𝑥))
84	83	ssrdv 3939	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑦(ball‘𝐷)1) ⊆ 𝑥)
85		oveq2 7366	. . . . . . . 8 ⊢ (𝑟 = 1 → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)1))
86	85	sseq1d 3965	. . . . . . 7 ⊢ (𝑟 = 1 → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ (𝑦(ball‘𝐷)1) ⊆ 𝑥))
87	86	rspcev 3576	. . . . . 6 ⊢ ((1 ∈ ℝ⁺ ∧ (𝑦(ball‘𝐷)1) ⊆ 𝑥) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
88	47, 84, 87	sylancr 587	. . . . 5 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
89	46, 88	pm2.61dan 812	. . . 4 ⊢ ((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
90	89	ralrimiva 3128	. . 3 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
91		xrsmopn.1	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
92	91	elmopn2 24389	. . . 4 ⊢ (𝐷 ∈ (∞Met‘ℝ^) → (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ^ ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
93	22, 92	ax-mp 5	. . 3 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ^* ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
94	3, 90, 93	sylanbrc 583	. 2 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ∈ 𝐽)
95	94	ssriv 3937	1 ⊢ (ordTop‘ ≤ ) ⊆ 𝐽

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∩ cin 3900 ⊆ wss 3901 ∪ cuni 4863 class class class wbr 5098 × cxp 5622 ran crn 5625 ↾ cres 5626 ∘ ccom 5628 ‘cfv 6492 (class class class)co 7358 ℝcr 11025 0cc0 11026 1c1 11027 ℝ^*cxr 11165 < clt 11166 ≤ cle 11167 − cmin 11364 ℝ⁺crp 12905 (,)cioo 13261 abscabs 15157 distcds 17186 ↾_t crest 17340 topGenctg 17357 ordTopcordt 17420 ℝ^*_𝑠cxrs 17421 ∞Metcxmet 21294 ballcbl 21296 MetOpencmopn 21299 Topctop 22837

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-er 8635 df-ec 8637 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9314 df-sup 9345 df-inf 9346 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-ioo 13265 df-ioc 13266 df-ico 13267 df-icc 13268 df-fz 13424 df-seq 13925 df-exp 13985 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-struct 17074 df-slot 17109 df-ndx 17121 df-base 17137 df-plusg 17190 df-mulr 17191 df-tset 17196 df-ple 17197 df-ds 17199 df-rest 17342 df-topgen 17363 df-ordt 17422 df-xrs 17423 df-ps 18489 df-tsr 18490 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-top 22838 df-topon 22855 df-bases 22890

This theorem is referenced by: xmetdcn 24783

W3C validator