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 25187

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 4904	. . . 4 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ⊆ ∪ (ordTop‘ ≤ ))
2		letopuni 23580	. . . 4 ⊢ ℝ^* = ∪ (ordTop‘ ≤ )
3	1, 2	sseqtrrdi 3954	. . 3 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ⊆ ℝ^*)
4		eqid 2763	. . . . . . . 8 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
5	4	rexmet 25165	. . . . . . 7 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
6		letop 23579	. . . . . . . . 9 ⊢ (ordTop‘ ≤ ) ∈ Top
7		reex 11330	. . . . . . . . 9 ⊢ ℝ ∈ V
8		elrestr 17649	. . . . . . . . 9 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ (ordTop‘ ≤ )) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
9	6, 7, 8	mp3an12 1481	. . . . . . . 8 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
10	9	ad2antrr 739	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
11		elin 4096	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑥 ∩ ℝ) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ))
12	11	biimpri 231	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ))
13	12	adantll 727	. . . . . . 7 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ (𝑥 ∩ ℝ))
14		eqid 2763	. . . . . . . . . 10 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = ((ordTop‘ ≤ ) ↾_t ℝ)
15	14	xrtgioo 25181	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾_t ℝ)
16		eqid 2763	. . . . . . . . . 10 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
17	4, 16	tgioo 25170	. . . . . . . . 9 ⊢ (topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
18	15, 17	eqtr3i 2788	. . . . . . . 8 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
19	18	mopni2 24867	. . . . . . 7 ⊢ ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑥 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ) ∧ 𝑦 ∈ (𝑥 ∩ ℝ)) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ))
20	5, 10, 13, 19	mp3an2i 1496	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ))
21		xrsxmet.1	. . . . . . . . . . . 12 ⊢ 𝐷 = (dist‘ℝ^*_𝑠)
22	21	xrsxmet 25184	. . . . . . . . . . 11 ⊢ 𝐷 ∈ (∞Met‘ℝ^*)
23		simplr 781	. . . . . . . . . . . 12 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ ℝ)
24		ressxr 11392	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℝ^*
25		sseqin2 4123	. . . . . . . . . . . . 13 ⊢ (ℝ ⊆ ℝ^* ↔ (ℝ^* ∩ ℝ) = ℝ)
26	24, 25	mpbi 233	. . . . . . . . . . . 12 ⊢ (ℝ^* ∩ ℝ) = ℝ
27	23, 26	eleqtrrdi 2875	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑦 ∈ (ℝ^* ∩ ℝ))
28		rpxr 13170	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
29	28	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ^*)
30	21	xrsdsre 25185	. . . . . . . . . . . . 13 ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
31	30	eqcomi 2772	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = (𝐷 ↾ (ℝ × ℝ))
32	31	blres 24805	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ (ℝ^ ∩ ℝ) ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ))
33	22, 27, 29, 32	mp3an2i 1496	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = ((𝑦(ball‘𝐷)𝑟) ∩ ℝ))
34	21	xrsblre 25186	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
35	28, 34	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
36	35	adantll 727	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘𝐷)𝑟) ⊆ ℝ)
37		dfss2 4097	. . . . . . . . . . 11 ⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ ℝ ↔ ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟))
38	36, 37	sylib 221	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘𝐷)𝑟) ∩ ℝ) = (𝑦(ball‘𝐷)𝑟))
39	33, 38	eqtrd 2798	. . . . . . . . 9 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (𝑦(ball‘𝐷)𝑟))
40	39	sseq1d 3944	. . . . . . . 8 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) ↔ (𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ)))
41		inss1 4136	. . . . . . . . 9 ⊢ (𝑥 ∩ ℝ) ⊆ 𝑥
42		sstr 3921	. . . . . . . . 9 ⊢ (((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) ∧ (𝑥 ∩ ℝ) ⊆ 𝑥) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
43	41, 42	mpan2 704	. . . . . . . 8 ⊢ ((𝑦(ball‘𝐷)𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
44	40, 43	biimtrdi 256	. . . . . . 7 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
45	44	reximdva 3179	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ⊆ (𝑥 ∩ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
46	20, 45	mpd 16	. . . . 5 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ 𝑦 ∈ ℝ) → ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
47		1rp 13164	. . . . . 6 ⊢ 1 ∈ ℝ⁺
48	3	sselda 3913	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℝ^*)
49	48	adantr 486	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ^*)
50		rpxr 13170	. . . . . . . . . 10 ⊢ (1 ∈ ℝ⁺ → 1 ∈ ℝ^*)
51	47, 50	mp1i 14	. . . . . . . . 9 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → 1 ∈ ℝ^*)
52		elbl 24762	. . . . . . . . 9 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 1 ∈ ℝ^) → (𝑧 ∈ (𝑦(ball‘𝐷)1) ↔ (𝑧 ∈ ℝ^ ∧ (𝑦𝐷𝑧) < 1)))
53	22, 49, 51, 52	mp3an2i 1496	. . . . . . . 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 24705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 𝑧 ∈ ℝ^) → (𝑦𝐷𝑧) ∈ ℝ^)
59	22, 56, 57, 58	mp3an2i 1496	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ^*)
60		1red 11348	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 1 ∈ ℝ)
61		xmetge0 24718	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ (∞Met‘ℝ^) ∧ 𝑦 ∈ ℝ^ ∧ 𝑧 ∈ ℝ^*) → 0 ≤ (𝑦𝐷𝑧))
62	22, 56, 57, 61	mp3an2i 1496	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 0 ≤ (𝑦𝐷𝑧))
63		simpl3r 1248	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) < 1)
64		1xr 11407	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ^*
65		xrltle 13318	. . . . . . . . . . . . . . . . . 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 13344	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦𝐷𝑧) ∈ ℝ^* ∧ 1 ∈ ℝ) ∧ (0 ≤ (𝑦𝐷𝑧) ∧ (𝑦𝐷𝑧) ≤ 1)) → (𝑦𝐷𝑧) ∈ ℝ)
69	59, 60, 62, 67, 68	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → (𝑦𝐷𝑧) ∈ ℝ)
70		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧)
71	21	xrsdsreclb 21772	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ∧ 𝑦 ≠ 𝑧) → ((𝑦𝐷𝑧) ∈ ℝ ↔ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)))
72	56, 57, 70, 71	syl3anc 1399	. . . . . . . . . . . . . . 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 2977	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → (¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧))
77		simp1r 1217	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ ∧ (𝑧 ∈ ℝ^* ∧ (𝑦𝐷𝑧) < 1)) → 𝑦 ∈ 𝑥)
78		elequ1 2154	. . . . . . . . . . . 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 3919	. . . . . 6 ⊢ (((𝑥 ∈ (ordTop‘ ≤ ) ∧ 𝑦 ∈ 𝑥) ∧ ¬ 𝑦 ∈ ℝ) → (𝑦(ball‘𝐷)1) ⊆ 𝑥)
85		oveq2 7459	. . . . . . . 8 ⊢ (𝑟 = 1 → (𝑦(ball‘𝐷)𝑟) = (𝑦(ball‘𝐷)1))
86	85	sseq1d 3944	. . . . . . 7 ⊢ (𝑟 = 1 → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ (𝑦(ball‘𝐷)1) ⊆ 𝑥))
87	86	rspcev 3580	. . . . . 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 3158	. . 3 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)
91		xrsmopn.1	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
92	91	elmopn2 24819	. . . 4 ⊢ (𝐷 ∈ (∞Met‘ℝ^) → (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ^ ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
93	22, 92	ax-mp 5	. . 3 ⊢ (𝑥 ∈ 𝐽 ↔ (𝑥 ⊆ ℝ^* ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))
94	3, 90, 93	sylanbrc 595	. 2 ⊢ (𝑥 ∈ (ordTop‘ ≤ ) → 𝑥 ∈ 𝐽)
95	94	ssriv 3917	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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∩ cin 4092 ∪ cuni 4872 class class class wbr 5108 × cxp 5656 ran crn 5659 ↾ cres 5660 ∘ ccom 5662 ‘cfv 6566 (class class class)co 7451 ℝcr 11238 0cc0 11239 1c1 11240 ℝ^*cxr 11381 < clt 11382 ≤ cle 11383 − cmin 11580 ℝ⁺crp 13160 (,)cioo 13516 abscabs 15444 distcds 17481 ↾_t crest 17641 topGenctg 17658 ordTopcordt 17721 ℝ^*_𝑠cxrs 17722 ∞Metcxmet 21714 ballcbl 21716 MetOpencmopn 21719 Topctop 23266

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-ec 8757 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fi 9440 df-sup 9471 df-inf 9472 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-ioo 13520 df-ioc 13521 df-ico 13522 df-icc 13523 df-fz 13680 df-seq 14185 df-exp 14245 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-struct 17369 df-slot 17404 df-ndx 17416 df-base 17432 df-plusg 17486 df-mulr 17487 df-tset 17492 df-ple 17493 df-ds 17495 df-rest 17643 df-topgen 17664 df-ordt 17723 df-xrs 17724 df-ps 18790 df-tsr 18791 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-top 23267 df-topon 23284 df-bases 23319

This theorem is used by: xmetdcn 25213

W3C validator