relowlssretop - Mathbox for ML

	Mathbox for ML		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > relowlssretop		Structured version Visualization version Unicode version

Theorem relowlssretop 31836

Description: The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.)

**Hypothesis**
Ref	Expression
relowlssretop.1

**Assertion**
Ref	Expression
relowlssretop

Proof of Theorem relowlssretop Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioof 11757	. . . . . 6
2		ffn 5739	. . . . . 6
3		ovelrn 6464	. . . . . 6
4	1, 2, 3	mp2b 10	. . . . 5
5		elxr 11439	. . . . . . . . . 10 $\/$ $\/$
6		simpr 468	. . . . . . . . . . . . . . . 16 $/\$
7		elioore 11691	. . . . . . . . . . . . . . . 16
8	6, 7	anim12ci 577	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		relowlssretop.1	. . . . . . . . . . . . . . . 16
10	9	icoreelrn 31834	. . . . . . . . . . . . . . 15 $/\$ $/\$
11	8, 10	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
12	7	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$
13	7	leidd 10201	. . . . . . . . . . . . . . . 16
14	13	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	6	rexrd 9708	. . . . . . . . . . . . . . . . . 18 $/\$
16		elioo1 11701	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	15, 16	syldan 478	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18	17	biimpa 492	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	simp3d 1044	. . . . . . . . . . . . . . 15 $/\$ $/\$
20		rexr 9704	. . . . . . . . . . . . . . . . . 18
21	20	3anim1i 1216	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
22		rexr 9704	. . . . . . . . . . . . . . . . . . 19
23		elico1 11704	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
24	20, 22, 23	syl2an 485	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
25	24	biimprd 231	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	8, 21, 25	syl2im 38	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
27		icoreval 31826	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	8, 27	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29	28	eleq2d 2534	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
30	26, 29	sylibd 222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
31	12, 14, 19, 30	mp3and 1393	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
32		nfv 1769	. . . . . . . . . . . . . . . 16 $/\$ $/\$
33		nfrab1 2957	. . . . . . . . . . . . . . . 16 $/\$
34		nfcv 2612	. . . . . . . . . . . . . . . 16
35		iooval 11685	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
36	35	eleq2d 2534	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
37	36	anbi1d 719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	pm5.32i 649	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		rabid 2953	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40		rabid 2953	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
41	39, 40	anbi12i 711	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43	42	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
44	43	ad2antll 743	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
46	45, 43	anim12i 576	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	anim2i 579	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48		3anass 1011	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
49	47, 48	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
51		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
52	50, 51	anim12i 576	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		xrltletr 11477	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
55	49, 53, 54	sylc 61	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
57	56	ad2antll 743	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 57	jca 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		rabid 2953	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
60	44, 58, 59	sylanbrc 677	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	adantlr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		iooval 11685	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	61, 63	eleqtrrd 2552	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	41, 64	sylan2b 483	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
66	38, 65	sylbi 200	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
67	66	expr 626	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
68	32, 33, 34, 67	ssrd 3423	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
69	22, 68	sylanl2 663	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
70		eleq2 2538	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71		sseq1 3439	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72	70, 71	anbi12d 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	rspcev 3136	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 31, 69, 73	syl12anc 1290	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
75	74	ancom1s 822	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
76	75	expl 630	. . . . . . . . . . 11 $/\$ $/\$
77	7	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$
78		peano2re 9824	. . . . . . . . . . . . . . . 16
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	9	icoreelrn 31834	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	77, 79, 80	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
82		elioore 11691	. . . . . . . . . . . . . . . . . . . . 21
83	82	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
84	83	leidd 10201	. . . . . . . . . . . . . . . . . . . 20 $/\$
85	83	ltp1d 10559	. . . . . . . . . . . . . . . . . . . 20 $/\$
86	83, 84, 85	jca32 544	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
87		breq2 4399	. . . . . . . . . . . . . . . . . . . . 21
88		breq1 4398	. . . . . . . . . . . . . . . . . . . . 21
89	87, 88	anbi12d 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
90	89	elrab 3184	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
91	86, 90	sylibr 217	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92		nfv 1769	. . . . . . . . . . . . . . . . . . 19 $/\$
93		nfrab1 2957	. . . . . . . . . . . . . . . . . . 19 $/\$
94		nfcv 2612	. . . . . . . . . . . . . . . . . . 19
95		rabid 2953	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
96		simprl 772	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
97		simpll 768	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
98	83	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
99	98	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
100	96	rexrd 9708	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
101		elioopnf 11753	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
102	101	simplbda 636	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
103	102	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
104		simprl 772	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
105	104	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
106	97, 99, 100, 103, 105	xrltletrd 11481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
107		elioopnf 11753	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
108	107	biimprd 231	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
109	108	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	96, 106, 110	mp2and 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	111	ex 441	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
113	95, 112	syl5bi 225	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114	92, 93, 94, 113	ssrd 3423	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
115	91, 114	jca 541	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
116		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20
117	116	eleq2d 2534	. . . . . . . . . . . . . . . . . . 19
118	117	anbi2d 718	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
119	116	sseq2d 3446	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
120	119	anbi2d 718	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	118, 120	imbi12d 327	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 121	mpbiri 241	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
123	122	impl 632	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
124	123	ancom1s 822	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125		eleq2 2538	. . . . . . . . . . . . . . . 16 $/\$ $/\$
126		sseq1 3439	. . . . . . . . . . . . . . . 16 $/\$ $/\$
127	125, 126	anbi12d 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	rspcev 3136	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	81, 124, 128	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	129	ancom1s 822	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	130	expl 630	. . . . . . . . . . 11 $/\$ $/\$
132	7	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
133		oveq2 6316	. . . . . . . . . . . . . . . . . . 19
134	133	eleq2d 2534	. . . . . . . . . . . . . . . . . 18
135	134	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$
136	135	pm5.32i 649	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
137		nltmnf 11454	. . . . . . . . . . . . . . . . . . . . 21
138	137	intnand 930	. . . . . . . . . . . . . . . . . . . 20 $/\$
139		eliooord 11719	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	138, 139	nsyl 125	. . . . . . . . . . . . . . . . . . 19
141	140	pm2.21d 109	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142	141	impd 438	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
143	142	ancomsd 461	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
144	136, 143	syl5bi 225	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
145	20, 144	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	132, 145	mpcom 36	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
147	146	ancom1s 822	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
148	147	expl 630	. . . . . . . . . . 11 $/\$ $/\$
149	76, 131, 148	3jaoi 1357	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
150	5, 149	sylbi 200	. . . . . . . . 9 $/\$ $/\$
151	150	expdimp 444	. . . . . . . 8 $/\$ $/\$
152	151	ancoms 460	. . . . . . 7 $/\$ $/\$
153		eleq2 2538	. . . . . . . 8
154		sseq2 3440	. . . . . . . . . 10
155	154	anbi2d 718	. . . . . . . . 9 $/\$ $/\$
156	155	rexbidv 2892	. . . . . . . 8 $/\$ $/\$
157	153, 156	imbi12d 327	. . . . . . 7 $/\$ $/\$
158	152, 157	syl5ibrcom 230	. . . . . 6 $/\$ $/\$
159	158	rexlimivv 2876	. . . . 5 $/\$
160	4, 159	sylbi 200	. . . 4 $/\$
161	160	rgen 2766	. . 3 $/\$
162	161	rgenw 2768	. 2 $/\$
163		iooex 11684	. . . . 5
164	163	rnex 6746	. . . 4
165		unirnioo 11759	. . . . 5
166	9	icoreunrn 31832	. . . . 5
167	165, 166	eqtr3i 2495	. . . 4
168		tgss2 20080	. . . 4 $/\$ $/\$
169	164, 167, 168	mp2an 686	. . 3 $/\$
170	165	raleqi 2977	. . 3 $/\$ $/\$
171	169, 170	bitr4i 260	. 2 $/\$
172	162, 171	mpbir 214	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $\/$ w3o 1006 $/\$ w3a 1007

wceq 1452

wcel 1904

wral 2756

wrex 2757

crab 2760

cvv 3031

wss 3390

cpw 3942

cuni 4190 class class class wbr 4395

cxp 4837

crn 4840

cima 4842

wfn 5584

wf 5585

cfv 5589 (class class class)co 6308

cr 9556

c1 9558

caddc 9560

cpnf 9690

cmnf 9691

cxr 9692

clt 9693

cle 9694

cioo 11660

cico 11662

ctg 15414

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-po 4760 df-so 4761 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-1st 6812 df-2nd 6813 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-ioo 11664 df-ico 11666 df-topgen 15420

This theorem is referenced by: relowlpssretop 31837

W3C validator