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 31766

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 11732	. . . . . 6
2		ffn 5728	. . . . . 6
3		ovelrn 6445	. . . . . 6
4	1, 2, 3	mp2b 10	. . . . 5
5		elxr 11416	. . . . . . . . . 10 $\/$ $\/$
6		simpr 463	. . . . . . . . . . . . . . . 16 $/\$
7		elioore 11666	. . . . . . . . . . . . . . . 16
8	6, 7	anim12ci 571	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		relowlssretop.1	. . . . . . . . . . . . . . . 16
10	9	icoreelrn 31764	. . . . . . . . . . . . . . 15 $/\$ $/\$
11	8, 10	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
12	7	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
13	7	leidd 10180	. . . . . . . . . . . . . . . 16
14	13	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	6	rexrd 9690	. . . . . . . . . . . . . . . . . 18 $/\$
16		elioo1 11676	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	15, 16	syldan 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18	17	biimpa 487	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	simp3d 1022	. . . . . . . . . . . . . . 15 $/\$ $/\$
20		rexr 9686	. . . . . . . . . . . . . . . . . 18
21	20	3anim1i 1194	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
22		rexr 9686	. . . . . . . . . . . . . . . . . . 19
23		elico1 11679	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
24	20, 22, 23	syl2an 480	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
25	24	biimprd 227	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	8, 21, 25	syl2im 39	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
27		icoreval 31756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	8, 27	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29	28	eleq2d 2514	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
30	26, 29	sylibd 218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
31	12, 14, 19, 30	mp3and 1367	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
32		nfv 1761	. . . . . . . . . . . . . . . 16 $/\$ $/\$
33		nfrab1 2971	. . . . . . . . . . . . . . . 16 $/\$
34		nfcv 2592	. . . . . . . . . . . . . . . 16
35		iooval 11660	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
36	35	eleq2d 2514	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
37	36	anbi1d 711	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	pm5.32i 643	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		rabid 2967	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40		rabid 2967	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
41	39, 40	anbi12i 703	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43	42	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
44	43	ad2antll 735	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
46	45, 43	anim12i 570	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	anim2i 573	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48		3anass 989	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
49	47, 48	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
51		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
52	50, 51	anim12i 570	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		xrltletr 11454	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
55	49, 53, 54	sylc 62	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simprr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
57	56	ad2antll 735	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 57	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		rabid 2967	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
60	44, 58, 59	sylanbrc 670	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	adantlr 721	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		iooval 11660	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	61, 63	eleqtrrd 2532	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	41, 64	sylan2b 478	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
66	38, 65	sylbi 199	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
67	66	expr 620	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
68	32, 33, 34, 67	ssrd 3437	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
69	22, 68	sylanl2 657	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
70		eleq2 2518	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71		sseq1 3453	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72	70, 71	anbi12d 717	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	rspcev 3150	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 31, 69, 73	syl12anc 1266	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
75	74	ancom1s 814	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
76	75	expl 624	. . . . . . . . . . 11 $/\$ $/\$
77	7	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
78		peano2re 9806	. . . . . . . . . . . . . . . 16
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	9	icoreelrn 31764	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	77, 79, 80	syl2anc 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
82		elioore 11666	. . . . . . . . . . . . . . . . . . . . 21
83	82	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
84	83	leidd 10180	. . . . . . . . . . . . . . . . . . . 20 $/\$
85	83	ltp1d 10537	. . . . . . . . . . . . . . . . . . . 20 $/\$
86	83, 84, 85	jca32 538	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
87		breq2 4406	. . . . . . . . . . . . . . . . . . . . 21
88		breq1 4405	. . . . . . . . . . . . . . . . . . . . 21
89	87, 88	anbi12d 717	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
90	89	elrab 3196	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
91	86, 90	sylibr 216	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92		nfv 1761	. . . . . . . . . . . . . . . . . . 19 $/\$
93		nfrab1 2971	. . . . . . . . . . . . . . . . . . 19 $/\$
94		nfcv 2592	. . . . . . . . . . . . . . . . . . 19
95		rabid 2967	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
96		simprl 764	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
97		simpll 760	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
98	83	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
99	98	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
100	96	rexrd 9690	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
101		elioopnf 11728	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
102	101	simplbda 630	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
103	102	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
104		simprl 764	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
105	104	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
106	97, 99, 100, 103, 105	xrltletrd 11458	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
107		elioopnf 11728	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
108	107	biimprd 227	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
109	108	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	96, 106, 110	mp2and 685	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	111	ex 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
113	95, 112	syl5bi 221	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114	92, 93, 94, 113	ssrd 3437	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
115	91, 114	jca 535	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
116		oveq2 6298	. . . . . . . . . . . . . . . . . . . 20
117	116	eleq2d 2514	. . . . . . . . . . . . . . . . . . 19
118	117	anbi2d 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
119	116	sseq2d 3460	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
120	119	anbi2d 710	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	118, 120	imbi12d 322	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 121	mpbiri 237	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
123	122	impl 626	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
124	123	ancom1s 814	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125		eleq2 2518	. . . . . . . . . . . . . . . 16 $/\$ $/\$
126		sseq1 3453	. . . . . . . . . . . . . . . 16 $/\$ $/\$
127	125, 126	anbi12d 717	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	rspcev 3150	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	81, 124, 128	syl2anc 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	129	ancom1s 814	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	130	expl 624	. . . . . . . . . . 11 $/\$ $/\$
132	7	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$
133		oveq2 6298	. . . . . . . . . . . . . . . . . . 19
134	133	eleq2d 2514	. . . . . . . . . . . . . . . . . 18
135	134	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
136	135	pm5.32i 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
137		nltmnf 11431	. . . . . . . . . . . . . . . . . . . . 21
138	137	intnand 927	. . . . . . . . . . . . . . . . . . . 20 $/\$
139		eliooord 11694	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	138, 139	nsyl 125	. . . . . . . . . . . . . . . . . . 19
141	140	pm2.21d 110	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
142	141	impd 433	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
143	142	ancomsd 456	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
144	136, 143	syl5bi 221	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
145	20, 144	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
146	132, 145	mpcom 37	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
147	146	ancom1s 814	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
148	147	expl 624	. . . . . . . . . . 11 $/\$ $/\$
149	76, 131, 148	3jaoi 1331	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
150	5, 149	sylbi 199	. . . . . . . . 9 $/\$ $/\$
151	150	expdimp 439	. . . . . . . 8 $/\$ $/\$
152	151	ancoms 455	. . . . . . 7 $/\$ $/\$
153		eleq2 2518	. . . . . . . 8
154		sseq2 3454	. . . . . . . . . 10
155	154	anbi2d 710	. . . . . . . . 9 $/\$ $/\$
156	155	rexbidv 2901	. . . . . . . 8 $/\$ $/\$
157	153, 156	imbi12d 322	. . . . . . 7 $/\$ $/\$
158	152, 157	syl5ibrcom 226	. . . . . 6 $/\$ $/\$
159	158	rexlimivv 2884	. . . . 5 $/\$
160	4, 159	sylbi 199	. . . 4 $/\$
161	160	rgen 2747	. . 3 $/\$
162	161	rgenw 2749	. 2 $/\$
163		iooex 11659	. . . . 5
164	163	rnex 6727	. . . 4
165		unirnioo 11734	. . . . 5
166	9	icoreunrn 31762	. . . . 5
167	165, 166	eqtr3i 2475	. . . 4
168		tgss2 20003	. . . 4 $/\$ $/\$
169	164, 167, 168	mp2an 678	. . 3 $/\$
170	165	raleqi 2991	. . 3 $/\$ $/\$
171	169, 170	bitr4i 256	. 2 $/\$
172	162, 171	mpbir 213	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $\/$ w3o 984 $/\$ w3a 985

wceq 1444

wcel 1887

wral 2737

wrex 2738

crab 2741

cvv 3045

wss 3404

cpw 3951

cuni 4198 class class class wbr 4402

cxp 4832

crn 4835

cima 4837

wfn 5577

wf 5578

cfv 5582 (class class class)co 6290

cr 9538

c1 9540

caddc 9542

cpnf 9672

cmnf 9673

cxr 9674

clt 9675

cle 9676

cioo 11635

cico 11637

ctg 15336

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-po 4755 df-so 4756 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-1st 6793 df-2nd 6794 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-ioo 11639 df-ico 11641 df-topgen 15342

This theorem is referenced by: relowlpssretop 31767

W3C validator