xrsmopn

Description: The metric on the extended reals generates a topology, but this does not match the order topology on RR* ; for example { +oo } 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)

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

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	⊢ 𝐷 = ( dist ‘ ℝ^*_𝑠 )
2		xrsmopn.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3		elssuni	⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → 𝑥 ⊆ ∪ ( ordTop ‘ ≤ ) )
4		letopuni	⊢ ℝ^* = ∪ ( ordTop ‘ ≤ )
5	3 4	sseqtrrdi	⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → 𝑥 ⊆ ℝ^* )
6		eqid	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
7	6	rexmet	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
8		letop	⊢ ( ordTop ‘ ≤ ) ∈ Top
9		reex	⊢ ℝ ∈ V
10		elrestr	⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑥 ∈ ( ordTop ‘ ≤ ) ) → ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) )
11	8 9 10	mp3an12	⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) )
12	11	ad2antrr	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) )
13		elin	⊢ ( 𝑦 ∈ ( 𝑥 ∩ ℝ ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ ) )
14	13	biimpri	⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ( 𝑥 ∩ ℝ ) )
15	14	adantll	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ( 𝑥 ∩ ℝ ) )
16		eqid	⊢ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) = ( ( ordTop ‘ ≤ ) ↾_t ℝ )
17	16	xrtgioo	⊢ ( topGen ‘ ran (,) ) = ( ( ordTop ‘ ≤ ) ↾_t ℝ )
18		eqid	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
19	6 18	tgioo	⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
20	17 19	eqtr3i	⊢ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
21	20	mopni2	⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ ( 𝑥 ∩ ℝ ) ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) ∧ 𝑦 ∈ ( 𝑥 ∩ ℝ ) ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) )
22	7 12 15 21	mp3an2i	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) )
23	1	xrsxmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ^* )
24		simplr	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → 𝑦 ∈ ℝ )
25		ressxr	⊢ ℝ ⊆ ℝ^*
26		sseqin2	⊢ ( ℝ ⊆ ℝ^* ↔ ( ℝ^* ∩ ℝ ) = ℝ )
27	25 26	mpbi	⊢ ( ℝ^* ∩ ℝ ) = ℝ
28	24 27	eleqtrrdi	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → 𝑦 ∈ ( ℝ^* ∩ ℝ ) )
29		rpxr	⊢ ( 𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^* )
30	29	adantl	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → 𝑟 ∈ ℝ^* )
31	1	xrsdsre	⊢ ( 𝐷 ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
32	31	eqcomi	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( 𝐷 ↾ ( ℝ × ℝ ) )
33	32	blres	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) ∧ 𝑦 ∈ ( ℝ^* ∩ ℝ ) ∧ 𝑟 ∈ ℝ^* ) → ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) )
34	23 28 30 33	mp3an2i	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) )
35	1	xrsblre	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ^* ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ )
36	29 35	sylan2	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ )
37	36	adantll	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ )
38		dfss2	⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ℝ ↔ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
39	37 38	sylib	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ∩ ℝ ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
40	34 39	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) )
41	40	sseq1d	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → ( ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) ↔ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) ) )
42		inss1	⊢ ( 𝑥 ∩ ℝ ) ⊆ 𝑥
43		sstr	⊢ ( ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) ∧ ( 𝑥 ∩ ℝ ) ⊆ 𝑥 ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
44	42 43	mpan2	⊢ ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
45	41 44	biimtrdi	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑟 ∈ ℝ⁺ ) → ( ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) )
46	45	reximdva	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ ( 𝑥 ∩ ℝ ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) )
47	22 46	mpd	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
48		1rp	⊢ 1 ∈ ℝ⁺
49	5	sselda	⊢ ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ℝ^* )
50	49	adantr	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ^* )
51		rpxr	⊢ ( 1 ∈ ℝ⁺ → 1 ∈ ℝ^* )
52	48 51	mp1i	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → 1 ∈ ℝ^* )
53		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) ∧ 𝑦 ∈ ℝ^* ∧ 1 ∈ ℝ^* ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) )
54	23 50 52 53	mp3an2i	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ↔ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) )
55		simp2	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ¬ 𝑦 ∈ ℝ )
56	49	3ad2ant1	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → 𝑦 ∈ ℝ^* )
57	56	adantr	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ ℝ^* )
58		simpl3l	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑧 ∈ ℝ^* )
59		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ^* )
60	23 57 58 59	mp3an2i	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ^* )
61		1red	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 1 ∈ ℝ )
62		xmetge0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) ∧ 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ) → 0 ≤ ( 𝑦 𝐷 𝑧 ) )
63	23 57 58 62	mp3an2i	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 0 ≤ ( 𝑦 𝐷 𝑧 ) )
64		simpl3r	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) < 1 )
65		1xr	⊢ 1 ∈ ℝ^*
66		xrltle	⊢ ( ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ^* ∧ 1 ∈ ℝ^* ) → ( ( 𝑦 𝐷 𝑧 ) < 1 → ( 𝑦 𝐷 𝑧 ) ≤ 1 ) )
67	60 65 66	sylancl	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝑦 𝐷 𝑧 ) < 1 → ( 𝑦 𝐷 𝑧 ) ≤ 1 ) )
68	64 67	mpd	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) ≤ 1 )
69		xrrege0	⊢ ( ( ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ^* ∧ 1 ∈ ℝ ) ∧ ( 0 ≤ ( 𝑦 𝐷 𝑧 ) ∧ ( 𝑦 𝐷 𝑧 ) ≤ 1 ) ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ )
70	60 61 63 68 69	syl22anc	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ )
71		simpr	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ≠ 𝑧 )
72	1	xrsdsreclb	⊢ ( ( 𝑦 ∈ ℝ^* ∧ 𝑧 ∈ ℝ^* ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ ↔ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) )
73	57 58 71 72	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝑦 𝐷 𝑧 ) ∈ ℝ ↔ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) )
74	70 73	mpbid	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) )
75	74	simpld	⊢ ( ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) ∧ 𝑦 ≠ 𝑧 ) → 𝑦 ∈ ℝ )
76	75	ex	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( 𝑦 ≠ 𝑧 → 𝑦 ∈ ℝ ) )
77	76	necon1bd	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( ¬ 𝑦 ∈ ℝ → 𝑦 = 𝑧 ) )
78		simp1r	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → 𝑦 ∈ 𝑥 )
79		elequ1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
80	78 79	syl5ibcom	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( 𝑦 = 𝑧 → 𝑧 ∈ 𝑥 ) )
81	77 80	syld	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → ( ¬ 𝑦 ∈ ℝ → 𝑧 ∈ 𝑥 ) )
82	55 81	mpd	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ∧ ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) ) → 𝑧 ∈ 𝑥 )
83	82	3expia	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ ℝ^* ∧ ( 𝑦 𝐷 𝑧 ) < 1 ) → 𝑧 ∈ 𝑥 ) )
84	54 83	sylbid	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) → 𝑧 ∈ 𝑥 ) )
85	84	ssrdv	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑥 )
86		oveq2	⊢ ( 𝑟 = 1 → ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝐷 ) 1 ) )
87	86	sseq1d	⊢ ( 𝑟 = 1 → ( ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ↔ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑥 ) )
88	87	rspcev	⊢ ( ( 1 ∈ ℝ⁺ ∧ ( 𝑦 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑥 ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
89	48 85 88	sylancr	⊢ ( ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) ∧ ¬ 𝑦 ∈ ℝ ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
90	47 89	pm2.61dan	⊢ ( ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
91	90	ralrimiva	⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 )
92	2	elmopn2	⊢ ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) → ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ⊆ ℝ^* ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) ) )
93	23 92	ax-mp	⊢ ( 𝑥 ∈ 𝐽 ↔ ( 𝑥 ⊆ ℝ^* ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑟 ∈ ℝ⁺ ( 𝑦 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑥 ) )
94	5 91 93	sylanbrc	⊢ ( 𝑥 ∈ ( ordTop ‘ ≤ ) → 𝑥 ∈ 𝐽 )
95	94	ssriv	⊢ ( ordTop ‘ ≤ ) ⊆ 𝐽

Metamath Proof Explorer

Theorem xrsmopn

Proof