relowlpssretop - Mathbox for ML

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

Theorem relowlpssretop 33212

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

**Hypothesis**
Ref	Expression
relowlpssretop.1

**Assertion**
Ref	Expression
relowlpssretop

Proof of Theorem relowlpssretop Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relowlpssretop.1	. . 3
2	1	relowlssretop 33211	. 2
3		2re 11090	. . . . 5
4		1lt2 11194	. . . . 5
5		ovex 6678	. . . . . . . . . . . 12
6		sbcan 3478	. . . . . . . . . . . . . . 15 $/\$ $/\$
7		1re 10039	. . . . . . . . . . . . . . . . 17
8		sbcg 3503	. . . . . . . . . . . . . . . . 17
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16
10		sbcbr123 4706	. . . . . . . . . . . . . . . . 17
11		csbvarg 4003	. . . . . . . . . . . . . . . . . . 19
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18
13		csbconstg 3546	. . . . . . . . . . . . . . . . . . 19
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18
15	12, 14	breq12i 4662	. . . . . . . . . . . . . . . . 17
16		csbconstg 3546	. . . . . . . . . . . . . . . . . . 19
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18
18	17	breqi 4659	. . . . . . . . . . . . . . . . 17
19	10, 15, 18	3bitri 286	. . . . . . . . . . . . . . . 16
20	9, 19	anbi12i 733	. . . . . . . . . . . . . . 15 $/\$ $/\$
21	6, 20	bitri 264	. . . . . . . . . . . . . 14 $/\$ $/\$
22		sbceqg 3984	. . . . . . . . . . . . . . . 16
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15
24		csbconstg 3546	. . . . . . . . . . . . . . . . 17
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16
26		csbov123 6687	. . . . . . . . . . . . . . . . 17
27		csbconstg 3546	. . . . . . . . . . . . . . . . . . 19
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18
29	12, 14, 28	oveq123i 6664	. . . . . . . . . . . . . . . . 17
30	26, 29	eqtri 2644	. . . . . . . . . . . . . . . 16
31	25, 30	eqeq12i 2636	. . . . . . . . . . . . . . 15
32	23, 31	bitri 264	. . . . . . . . . . . . . 14
33		sbcan 3478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
34		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
35		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
36		leid 10133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
37	35, 36	jccir 562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
38		rexr 10085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
39		elico2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
40	38, 39	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
41		df-3an 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
42	40, 41	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
43	42	baibd 948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
44	37, 43	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
45	44	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
46	45	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
47		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
48	47	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
49	46, 48	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
50		rexpssxrxp 10084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
51		opelxpi 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
52	50, 51	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
53		df-ico 12181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
54	53	ixxf 12185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55	54	fdmi 6052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
56	55	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
57	53	mpt2fun 6762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
58		funfvima 6492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
59	57, 58	mpan 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
60	56, 59	sylbir 225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	52, 51, 60	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
62		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62, 1	3eltr4g 2718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
64		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
65	63, 64	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
66	65	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
67		ioof 12271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
68		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
70		ovelrn 6810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
72		iooelexlt 33210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
73		df-rex 2918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
74	72, 73	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
75		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
77	53	elmpt2cl2 6878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
78		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
79		elico2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 $/\$ $/\$ $/\$
80	78, 79	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$ $/\$
81		simp2 1062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$
82	80, 81	syl6bi 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 $/\$
83	82	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
84	83	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
85	77, 84	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
86	85	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$
87	78	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
88	87	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
89		elicore 12226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$
90	78, 89	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$
91	90	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
92		xrlenlt 10103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$
93	92	biimpd 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$
94	93	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
95	88, 91, 94	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$
96	86, 95	mt2d 131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$
97	96	intnand 962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
98	97	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$
99	98	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
100	76, 99	jcad 555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
101		annim 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
102	100, 101	syl6ib 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
103	102	eximdv 1846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
104	74, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
105		exnal 1754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
106	104, 105	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
107		dfss2 3591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
108	106, 107	sylnibr 319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
109		imnan 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
110	108, 109	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
111		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
112		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
113	111, 112	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
114	110, 113	mtbiri 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
115		sseq2 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
116	115	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
117	116	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
118	114, 117	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
120	119	rexlimivv 3036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
121	71, 120	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
122	121	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
123	122	ralrimiv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
124		ralnex 2992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
125	123, 124	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
126	125	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
127	66, 126	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
128	127	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
129	49, 128	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130		an12 838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131		annim 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
132	131	anbi2i 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
133	130, 132	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
134	129, 133	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
135		rspe 3003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
137		rexnal 2995	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	136, 137	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
139	138	exp41 638	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140	139	com4l 92	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
141	140	imp41 619	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
142		rspe 3003	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	34, 141, 142	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
144		rexnal 2995	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
145	143, 144	sylib 208	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
146		df-ico 12181	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
147	146	ixxex 12186	. . . . . . . . . . . . . . . . . . . . . . . 24
148		imaexg 7103	. . . . . . . . . . . . . . . . . . . . . . . 24
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
150	1, 149	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . 22
151	1	icoreunrn 33207	. . . . . . . . . . . . . . . . . . . . . . 23
152		unirnioo 12273	. . . . . . . . . . . . . . . . . . . . . . 23
153	151, 152	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . . 22
154		tgss2 20791	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
155	150, 153, 154	mp2an 708	. . . . . . . . . . . . . . . . . . . . 21 $/\$
156	151	raleqi 3142	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
157	155, 156	bitr4i 267	. . . . . . . . . . . . . . . . . . . 20 $/\$
158	145, 157	sylnibr 319	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
159	158	sbcth 3450	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
161		sbcimg 3477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	7, 161	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	160, 162	mpbi 220	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
164		sbcel1v 3495	. . . . . . . . . . . . . . . . . 18
165	7, 164	mpbir 221	. . . . . . . . . . . . . . . . 17
166		sbcan 3478	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	165, 166	mpbiran2 954	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
168		sbcg 3503	. . . . . . . . . . . . . . . . 17
169	7, 168	ax-mp 5	. . . . . . . . . . . . . . . 16
170	163, 167, 169	3imtr3i 280	. . . . . . . . . . . . . . 15 $/\$ $/\$
171	33, 170	sylbir 225	. . . . . . . . . . . . . 14 $/\$ $/\$
172	21, 32, 171	syl2anbr 497	. . . . . . . . . . . . 13 $/\$ $/\$
173	172	sbcth 3450	. . . . . . . . . . . 12 $/\$ $/\$
174	5, 173	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$
175		sbcimg 3477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
176	5, 175	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
177	174, 176	mpbi 220	. . . . . . . . . 10 $/\$ $/\$
178		sbcan 3478	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179		eqid 2622	. . . . . . . . . . . . 13
180		eqsbc3 3475	. . . . . . . . . . . . . 14
181	5, 180	ax-mp 5	. . . . . . . . . . . . 13
182	179, 181	mpbir 221	. . . . . . . . . . . 12
183		sbcg 3503	. . . . . . . . . . . . . 14 $/\$ $/\$
184	5, 183	ax-mp 5	. . . . . . . . . . . . 13 $/\$ $/\$
185	184	anbi1i 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
186	182, 185	mpbiran2 954	. . . . . . . . . . 11 $/\$ $/\$ $/\$
187	178, 186	bitri 264	. . . . . . . . . 10 $/\$ $/\$ $/\$
188		sbcg 3503	. . . . . . . . . . 11
189	5, 188	ax-mp 5	. . . . . . . . . 10
190	177, 187, 189	3imtr3i 280	. . . . . . . . 9 $/\$
191	190	sbcth 3450	. . . . . . . 8 $/\$
192	3, 191	ax-mp 5	. . . . . . 7 $/\$
193		sbcimg 3477	. . . . . . . 8 $/\$ $/\$
194	3, 193	ax-mp 5	. . . . . . 7 $/\$ $/\$
195	192, 194	mpbi 220	. . . . . 6 $/\$
196		sbcan 3478	. . . . . . 7 $/\$ $/\$
197		sbcel1v 3495	. . . . . . . 8
198		sbcbr123 4706	. . . . . . . . 9
199		csbconstg 3546	. . . . . . . . . . 11
200	3, 199	ax-mp 5	. . . . . . . . . 10
201		csbvarg 4003	. . . . . . . . . . 11
202	3, 201	ax-mp 5	. . . . . . . . . 10
203	200, 202	breq12i 4662	. . . . . . . . 9
204		csbconstg 3546	. . . . . . . . . . 11
205	3, 204	ax-mp 5	. . . . . . . . . 10
206	205	breqi 4659	. . . . . . . . 9
207	198, 203, 206	3bitri 286	. . . . . . . 8
208	197, 207	anbi12i 733	. . . . . . 7 $/\$ $/\$
209	196, 208	bitri 264	. . . . . 6 $/\$ $/\$
210		sbcg 3503	. . . . . . 7
211	3, 210	ax-mp 5	. . . . . 6
212	195, 209, 211	3imtr3i 280	. . . . 5 $/\$
213	3, 4, 212	mp2an 708	. . . 4
214		eqimss 3657	. . . 4
215	213, 214	mto 188	. . 3
216	215	nesymir 2852	. 2
217		df-pss 3590	. 2 $/\$
218	2, 216, 217	mpbir2an 955	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

wsbc 3435

csb 3533

wss 3574

wpss 3575

cpw 4158

cop 4183

cuni 4436 class class class wbr 4653

cxp 5112

cdm 5114

crn 5115

cima 5117

wfun 5882

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cr 9935

c1 9937

cxr 10073

clt 10074

cle 10075

c2 11070

cioo 12175

cico 12177

ctg 16098

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-po 5035 df-so 5036 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-2 11079 df-ioo 12179 df-ico 12181 df-topgen 16104

This theorem is referenced by: (None)

W3C validator