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 25023

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 4906	. . . 4 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ⊆ ∪ (ordTop‘ ≤ ))
2		letopuni 23416	. . . 4 ⊢ ℝ^* = ∪ (ordTop‘ ≤ )
3	1, 2	sseqtrrdi 3979	. . 3 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ⊆ ℝ^*)
4		eqid 2765	. . . . . . . 8 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
5	4	rexmet 25001	. . . . . . 7 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
6		letop 23415	. . . . . . . . 9 ⊢ (ordTop‘ ≤ ) ∈ Top
7		reex 11208	. . . . . . . . 9 ⊢ ℝ ∈ V
8		elrestr 17505	. . . . . . . . 9 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ (ordTop‘ ≤ )) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
9	6, 7, 8	mp3an12 1480	. . . . . . . 8 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
10	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
11		elin 3922	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑥 ∩ ℝ) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ))
12	11	biimpri 231	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ))
13	12	adantll 727	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ))
14		eqid 2765	. . . . . . . . . 10 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = ((ordTop‘ ≤ ) ↾_t ℝ)
15	14	xrtgioo 25017	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾_t ℝ)
16		eqid 2765	. . . . . . . . . 10 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
17	4, 16	tgioo 25006	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
18	15, 17	eqtr3i 2790	. . . . . . . 8 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
19	18	mopni2 24703	. . . . . . 7 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ) ∧ 𝑦 ∈ (𝑥 ∩ ℝ)) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ))
20	5, 10, 13, 19	mp3an2i 1495	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ))
21		xrsxmet.1	. . . . . . . . . . . 12 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
22	21	xrsxmet 25020	. . . . . . . . . . 11 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)
23		simplr 781	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ ℝ)
24		ressxr 11270	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℝ^*
25		sseqin2 4176	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℝ^* ↔ (ℝ^* ∩ ℝ) = ℝ)
26	24, 25	mpbi 233	. . . . . . . . . . . 12 ⊢ (ℝ^* ∩ ℝ) = ℝ
27	23, 26	eleqtrrdi 2876	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ (ℝ^* ∩ ℝ))
28		rpxr 13044	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
29	28	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ^*)
30	21	xrsdsre 25021	. . . . . . . . . . . . 13 ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	eqcomi 2774	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = (𝐷 ↾ (ℝ × ℝ))
32	31	blres 24641	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ (ℝ^ ∩ ℝ) ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ))
33	22, 27, 29, 32	mp3an2i 1495	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ))
34	21	xrsblre 25022	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
35	28, 34	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
36	35	adantll 727	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
37		dfss2 3924	. . . . . . . . . . 11 ⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ ℝ ↔ ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟))
38	36, 37	sylib 221	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟))
39	33, 38	eqtrd 2800	. . . . . . . . 9 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (𝑦(ball‘𝐷)𝑟))
40	39	sseq1d 3969	. . . . . . . 8 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) ↔ (𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ)))
41		inss1 4189	. . . . . . . . 9 ⊢ (𝑥 ∩ ℝ) ⊆ 𝑥
42		sstr 3946	. . . . . . . . 9 ⊢ (((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) ∧ (𝑥 ∩ ℝ) ⊆ 𝑥) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
43	41, 42	mpan2 704	. . . . . . . 8 ⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
44	40, 43	biimtrdi 256	. . . . . . 7 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
45	44	reximdva 3180	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
46	20, 45	mpd 16	. . . . 5 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
47		1rp 13038	. . . . . 6 ⊢ 1 ∈ ℝ⁺
48	3	sselda 3938	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℝ^*)
49	48	adantr 486	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ^*)
50		rpxr 13044	. . . . . . . . . 10 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
51	47, 50	mp1i 14	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 1 ∈ ℝ^*)
52		elbl 24598	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 1 ∈ ℝ^) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ^ ∧ (𝑦𝐷𝑧) < 1)))
53	22, 49, 51, 52	mp3an2i 1495	. . . . . . . 8 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)))
54		simp2 1155	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → ¬ 𝑦 ∈ ℝ)
55	48	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ ℝ^*)
56	55	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ^*)
57		simpl3l 1247	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ ℝ^*)
58		xmetcl 24541	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 𝑧 ∈ ℝ^) → (𝑦𝐷𝑧) ∈ ℝ^)
59	22, 56, 57, 58	mp3an2i 1495	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ^*)
60		1red 11226	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 1 ∈ ℝ)
61		xmetge0 24554	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 𝑧 ∈ ℝ^*) → 0 ≤ (𝑦𝐷𝑧))
62	22, 56, 57, 61	mp3an2i 1495	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 0 ≤ (𝑦𝐷𝑧))
63		simpl3r 1248	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) < 1)
64		1xr 11285	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ^*
65		xrltle 13192	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦𝐷𝑧) ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1))
66	59, 64, 65	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) < 1 → (𝑦𝐷𝑧) ≤ 1))
67	63, 66	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ≤ 1)
68		xrrege0 13218	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦𝐷𝑧) ∈ ℝ^* ∧ 1 ∈ ℝ) ∧ (0 ≤ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≤ 1)) → (𝑦𝐷𝑧) ∈ ℝ)
69	59, 60, 62, 67, 68	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ)
70		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧)
71	21	xrsdsreclb 21616	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
72	56, 57, 70, 71	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
73	69, 72	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ))
74	73	simpld 500	. . . . . . . . . . . . 13 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ ℝ)
75	74	ex 418	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ))
76	75	necon1bd 2978	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧))
77		simp1r 1217	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ 𝑥)
78		elequ1 2153	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
79	77, 78	syl5ibcom 248	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (𝑦 = 𝑧 → 𝑧 ∈ 𝑥))
80	76, 79	syld 48	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥))
81	54, 80	mpd 16	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑧 ∈ 𝑥)
82	81	3expia 1139	. . . . . . . 8 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ((𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1) → 𝑧 ∈ 𝑥))
83	53, 82	sylbid 243	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝑦(ball‘𝐷)1) → 𝑧 ∈ 𝑥))
84	83	ssrdv 3944	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑦(ball‘𝐷)1) ⊆ 𝑥)
85		oveq2 7427	. . . . . . . 8 ⊢ (𝑟 = 1 → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)1))
86	85	sseq1d 3969	. . . . . . 7 ⊢ (𝑟 = 1 → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ (𝑦(ball‘𝐷)1) ⊆ 𝑥))
87	86	rspcev 3583	. . . . . 6 ⊢ ((1 ∈ ℝ⁺ ∧ (𝑦(ball‘𝐷)1) ⊆ 𝑥) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
88	47, 84, 87	sylancr 599	. . . . 5 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
89	46, 88	pm2.61dan 825	. . . 4 ⊢ ((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
90	89	ralrimiva 3159	. . 3 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
91		xrsmopn.1	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
92	91	elmopn2 24655	. . . 4 ⊢ (𝐷 ∈ (∞Met‘ℝ^) → (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ^ ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
93	22, 92	ax-mp 5	. . 3 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ^* ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
94	3, 90, 93	sylanbrc 595	. 2 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ∈ 𝐽)
95	94	ssriv 3942	1 ⊢ (ordTop‘ ≤ ) ⊆ 𝐽

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ∩ cin 3905 ⊆ wss 3906 ∪ cuni 4874 class class class wbr 5111 × cxp 5661 ran crn 5664 ↾ cres 5665 ∘ ccom 5667 ‘cfv 6540 (class class class)co 7419 ℝcr 11116 0cc0 11117 1c1 11118 ℝ^*cxr 11259 < clt 11260 ≤ cle 11261 − cmin 11458 ℝ⁺crp 13034 (,)cioo 13390 abscabs 15311 distcds 17343 ↾_t crest 17497 topGenctg 17514 ordTopcordt 17577 ℝ^*_𝑠cxrs 17578 ∞Metcxmet 21559 ballcbl 21561 MetOpencmopn 21564 Topctop 23102

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-pre-sup 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-ec 8702 df-map 8832 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fi 9378 df-sup 9409 df-inf 9410 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12522 df-z 12609 df-dec 12730 df-uz 12881 df-q 12991 df-rp 13035 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13394 df-ioc 13395 df-ico 13396 df-icc 13397 df-fz 13554 df-seq 14058 df-exp 14118 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-struct 17231 df-slot 17266 df-ndx 17278 df-base 17294 df-plusg 17347 df-mulr 17348 df-tset 17353 df-ple 17354 df-ds 17356 df-rest 17499 df-topgen 17520 df-ordt 17579 df-xrs 17580 df-ps 18646 df-tsr 18647 df-psmet 21566 df-xmet 21567 df-met 21568 df-bl 21569 df-mopn 21570 df-top 23103 df-topon 23120 df-bases 23155

This theorem is used by: xmetdcn 25049

W3C validator