relowlssretop - Mathbox for ML

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

Theorem relowlssretop 31713

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 11734	. . . . . 6
2		ffn 5744	. . . . . 6
3		ovelrn 6457	. . . . . 6
4	1, 2, 3	mp2b 10	. . . . 5
5		elxr 11418	. . . . . . . . . 10 $\/$ $\/$
6		simpr 463	. . . . . . . . . . . . . . . 16 $/\$
7		elioore 11668	. . . . . . . . . . . . . . . 16
8	6, 7	anim12ci 570	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
9		relowlssretop.1	. . . . . . . . . . . . . . . 16
10	9	icoreelrn 31711	. . . . . . . . . . . . . . 15 $/\$ $/\$
11	8, 10	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
12	7	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
13	7	leidd 10182	. . . . . . . . . . . . . . . 16
14	13	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
15	6	rexrd 9692	. . . . . . . . . . . . . . . . . 18 $/\$
16		elioo1 11678	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17	15, 16	syldan 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
18	17	biimpa 487	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
19	18	simp3d 1020	. . . . . . . . . . . . . . 15 $/\$ $/\$
20		rexr 9688	. . . . . . . . . . . . . . . . . 18
21	20	3anim1i 1192	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
22		rexr 9688	. . . . . . . . . . . . . . . . . . 19
23		elico1 11681	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
24	20, 22, 23	syl2an 480	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
25	24	biimprd 227	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
26	8, 21, 25	syl2im 40	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
27		icoreval 31703	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
28	8, 27	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
29	28	eleq2d 2493	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
30	26, 29	sylibd 218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
31	12, 14, 19, 30	mp3and 1364	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
32		nfv 1752	. . . . . . . . . . . . . . . 16 $/\$ $/\$
33		nfrab1 3010	. . . . . . . . . . . . . . . 16 $/\$
34		nfcv 2585	. . . . . . . . . . . . . . . 16
35		iooval 11662	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
36	35	eleq2d 2493	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
37	36	anbi1d 710	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38	37	pm5.32i 642	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39		rabid 3006	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
40		rabid 3006	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
41	39, 40	anbi12i 702	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43	42	rexrd 9692	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
44	43	ad2antll 734	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
46	45, 43	anim12i 569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	anim2i 572	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48		3anass 987	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
49	47, 48	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50		simprl 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
51		simprl 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
52	50, 51	anim12i 569	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		xrltletr 11456	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
55	49, 53, 54	sylc 63	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56		simprr 765	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
57	56	ad2antll 734	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 57	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		rabid 3006	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
60	44, 58, 59	sylanbrc 669	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	60	adantlr 720	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		iooval 11662	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
63	62	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64	61, 63	eleqtrrd 2514	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65	41, 64	sylan2b 478	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
66	38, 65	sylbi 199	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
67	66	expr 619	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
68	32, 33, 34, 67	ssrd 3470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
69	22, 68	sylanl2 656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
70		eleq2 2496	. . . . . . . . . . . . . . . 16 $/\$ $/\$
71		sseq1 3486	. . . . . . . . . . . . . . . 16 $/\$ $/\$
72	70, 71	anbi12d 716	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
73	72	rspcev 3183	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	11, 31, 69, 73	syl12anc 1263	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
75	74	ancom1s 813	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
76	75	expl 623	. . . . . . . . . . 11 $/\$ $/\$
77	7	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
78		peano2re 9808	. . . . . . . . . . . . . . . 16
79	77, 78	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	9	icoreelrn 31711	. . . . . . . . . . . . . . 15 $/\$ $/\$
81	77, 79, 80	syl2anc 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
82		elioore 11668	. . . . . . . . . . . . . . . . . . . . 21
83	82	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
84	83	leidd 10182	. . . . . . . . . . . . . . . . . . . 20 $/\$
85	83	ltp1d 10539	. . . . . . . . . . . . . . . . . . . 20 $/\$
86	83, 84, 85	jca32 538	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
87		breq2 4425	. . . . . . . . . . . . . . . . . . . . 21
88		breq1 4424	. . . . . . . . . . . . . . . . . . . . 21
89	87, 88	anbi12d 716	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
90	89	elrab 3230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
91	86, 90	sylibr 216	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92		nfv 1752	. . . . . . . . . . . . . . . . . . 19 $/\$
93		nfrab1 3010	. . . . . . . . . . . . . . . . . . 19 $/\$
94		nfcv 2585	. . . . . . . . . . . . . . . . . . 19
95		rabid 3006	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
96		simprl 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
97		simpll 759	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
98	83	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
99	98	rexrd 9692	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
100	96	rexrd 9692	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
101		elioopnf 11730	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
102	101	simplbda 629	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
103	102	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
104		simprl 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
105	104	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
106	97, 99, 100, 103, 105	xrltletrd 11460	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
107		elioopnf 11730	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
108	107	biimprd 227	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
109	108	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
110	109	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
111	96, 106, 110	mp2and 684	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	111	ex 436	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
113	95, 112	syl5bi 221	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
114	92, 93, 94, 113	ssrd 3470	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
115	91, 114	jca 535	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
116		oveq2 6311	. . . . . . . . . . . . . . . . . . . 20
117	116	eleq2d 2493	. . . . . . . . . . . . . . . . . . 19
118	117	anbi2d 709	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
119	116	sseq2d 3493	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
120	119	anbi2d 709	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	118, 120	imbi12d 322	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122	115, 121	mpbiri 237	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
123	122	impl 625	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
124	123	ancom1s 813	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
125		eleq2 2496	. . . . . . . . . . . . . . . 16 $/\$ $/\$
126		sseq1 3486	. . . . . . . . . . . . . . . 16 $/\$ $/\$
127	125, 126	anbi12d 716	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
128	127	rspcev 3183	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	81, 124, 128	syl2anc 666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
130	129	ancom1s 813	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
131	130	expl 623	. . . . . . . . . . 11 $/\$ $/\$
132	7	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$
133		oveq2 6311	. . . . . . . . . . . . . . . . . . 19
134	133	eleq2d 2493	. . . . . . . . . . . . . . . . . 18
135	134	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$
136	135	pm5.32i 642	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
137		nltmnf 11433	. . . . . . . . . . . . . . . . . . . . 21
138	137	intnand 925	. . . . . . . . . . . . . . . . . . . 20 $/\$
139		eliooord 11696	. . . . . . . . . . . . . . . . . . . 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 38	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
147	146	ancom1s 813	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
148	147	expl 623	. . . . . . . . . . 11 $/\$ $/\$
149	76, 131, 148	3jaoi 1328	. . . . . . . . . 10 $\/$ $\/$ $/\$ $/\$
150	5, 149	sylbi 199	. . . . . . . . 9 $/\$ $/\$
151	150	expdimp 439	. . . . . . . 8 $/\$ $/\$
152	151	ancoms 455	. . . . . . 7 $/\$ $/\$
153		eleq2 2496	. . . . . . . 8
154		sseq2 3487	. . . . . . . . . 10
155	154	anbi2d 709	. . . . . . . . 9 $/\$ $/\$
156	155	rexbidv 2940	. . . . . . . 8 $/\$ $/\$
157	153, 156	imbi12d 322	. . . . . . 7 $/\$ $/\$
158	152, 157	syl5ibrcom 226	. . . . . 6 $/\$ $/\$
159	158	rexlimivv 2923	. . . . 5 $/\$
160	4, 159	sylbi 199	. . . 4 $/\$
161	160	rgen 2786	. . 3 $/\$
162	161	rgenw 2787	. 2 $/\$
163		iooex 11661	. . . . 5
164	163	rnex 6739	. . . 4
165		unirnioo 11736	. . . . 5
166	9	icoreunrn 31709	. . . . 5
167	165, 166	eqtr3i 2454	. . . 4
168		tgss2 19995	. . . 4 $/\$ $/\$
169	164, 167, 168	mp2an 677	. . 3 $/\$
170	165	raleqi 3030	. . 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 982 $/\$ w3a 983

wceq 1438

wcel 1869

wral 2776

wrex 2777

crab 2780

cvv 3082

wss 3437

cpw 3980

cuni 4217 class class class wbr 4421

cxp 4849

crn 4852

cima 4854

wfn 5594

wf 5595

cfv 5599 (class class class)co 6303

cr 9540

c1 9542

caddc 9544

cpnf 9674

cmnf 9675

cxr 9676

clt 9677

cle 9678

cioo 11637

cico 11639

ctg 15329

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1666 ax-4 1679 ax-5 1749 ax-6 1795 ax-7 1840 ax-8 1871 ax-9 1873 ax-10 1888 ax-11 1893 ax-12 1906 ax-13 2054 ax-ext 2401 ax-sep 4544 ax-nul 4553 ax-pow 4600 ax-pr 4658 ax-un 6595 ax-cnex 9597 ax-resscn 9598 ax-1cn 9599 ax-icn 9600 ax-addcl 9601 ax-addrcl 9602 ax-mulcl 9603 ax-mulrcl 9604 ax-mulcom 9605 ax-addass 9606 ax-mulass 9607 ax-distr 9608 ax-i2m1 9609 ax-1ne0 9610 ax-1rid 9611 ax-rnegex 9612 ax-rrecex 9613 ax-cnre 9614 ax-pre-lttri 9615 ax-pre-lttrn 9616 ax-pre-ltadd 9617 ax-pre-mulgt0 9618

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 984 df-3an 985 df-tru 1441 df-ex 1661 df-nf 1665 df-sb 1788 df-eu 2270 df-mo 2271 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2573 df-ne 2621 df-nel 2622 df-ral 2781 df-rex 2782 df-reu 2783 df-rab 2785 df-v 3084 df-sbc 3301 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3763 df-if 3911 df-pw 3982 df-sn 3998 df-pr 4000 df-op 4004 df-uni 4218 df-iun 4299 df-br 4422 df-opab 4481 df-mpt 4482 df-id 4766 df-po 4772 df-so 4773 df-xp 4857 df-rel 4858 df-cnv 4859 df-co 4860 df-dm 4861 df-rn 4862 df-res 4863 df-ima 4864 df-iota 5563 df-fun 5601 df-fn 5602 df-f 5603 df-f1 5604 df-fo 5605 df-f1o 5606 df-fv 5607 df-riota 6265 df-ov 6306 df-oprab 6307 df-mpt2 6308 df-1st 6805 df-2nd 6806 df-er 7369 df-en 7576 df-dom 7577 df-sdom 7578 df-pnf 9679 df-mnf 9680 df-xr 9681 df-ltxr 9682 df-le 9683 df-sub 9864 df-neg 9865 df-ioo 11641 df-ico 11643 df-topgen 15335

This theorem is referenced by: relowlpssretop 31714

W3C validator