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 31813

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 31812	. 2
3		2re 10712	. . . . 5
4		1lt2 10810	. . . . 5
5		ovex 6348	. . . . . . . . . . . 12
6		sbcan 3322	. . . . . . . . . . . . . . 15 $/\$ $/\$
7		1re 9673	. . . . . . . . . . . . . . . . 17
8		sbcg 3345	. . . . . . . . . . . . . . . . 17
9	7, 8	ax-mp 5	. . . . . . . . . . . . . . . 16
10		sbcbr123 4470	. . . . . . . . . . . . . . . . 17
11		csbvarg 3804	. . . . . . . . . . . . . . . . . . 19
12	7, 11	ax-mp 5	. . . . . . . . . . . . . . . . . 18
13		csbconstg 3388	. . . . . . . . . . . . . . . . . . 19
14	7, 13	ax-mp 5	. . . . . . . . . . . . . . . . . 18
15	12, 14	breq12i 4427	. . . . . . . . . . . . . . . . 17
16		csbconstg 3388	. . . . . . . . . . . . . . . . . . 19
17	7, 16	ax-mp 5	. . . . . . . . . . . . . . . . . 18
18	17	breqi 4424	. . . . . . . . . . . . . . . . 17
19	10, 15, 18	3bitri 279	. . . . . . . . . . . . . . . 16
20	9, 19	anbi12i 708	. . . . . . . . . . . . . . 15 $/\$ $/\$
21	6, 20	bitri 257	. . . . . . . . . . . . . 14 $/\$ $/\$
22		sbceqg 3785	. . . . . . . . . . . . . . . 16
23	7, 22	ax-mp 5	. . . . . . . . . . . . . . 15
24		csbconstg 3388	. . . . . . . . . . . . . . . . 17
25	7, 24	ax-mp 5	. . . . . . . . . . . . . . . 16
26		csbov123 6354	. . . . . . . . . . . . . . . . 17
27		csbconstg 3388	. . . . . . . . . . . . . . . . . . 19
28	7, 27	ax-mp 5	. . . . . . . . . . . . . . . . . 18
29	12, 14, 28	oveq123i 6334	. . . . . . . . . . . . . . . . 17
30	26, 29	eqtri 2484	. . . . . . . . . . . . . . . 16
31	25, 30	eqeq12i 2476	. . . . . . . . . . . . . . 15
32	23, 31	bitri 257	. . . . . . . . . . . . . 14
33		sbcan 3322	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
34		simpr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
35		simpl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
36		leid 9760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
37	35, 36	jccir 546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
38		rexr 9717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
39		elico2 11732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
40	38, 39	sylan2 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
41		df-3an 993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
42	40, 41	syl6bb 269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
43	42	baibd 925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
44	37, 43	mpdan 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
45	44	biimpar 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
46	45	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
47		eleq2 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
48	47	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
49	46, 48	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
50		rexpssxrxp 9716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
51		opelxpi 4888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
52	50, 51	sseldi 3442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
53		df-ico 11675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
54	53	ixxf 11679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55	54	fdmi 5761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
56	55	eleq2i 2532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
57	53	mpt2fun 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
58		funfvima 6170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
59	57, 58	mpan 681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
60	56, 59	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
61	52, 51, 60	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
62		df-ov 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	61, 62, 1	3eltr4g 2557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
64		eleq1 2528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
65	63, 64	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
66	65	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
67		ioof 11766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
68		ffn 5755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
69	67, 68	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
70		ovelrn 6477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
72		iooelexlt 31811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
73		df-rex 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
74	72, 73	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
75		simpl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
77	53	elmpt2cl2 6545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
78		elioore 11700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
79		elico2 11732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 $/\$ $/\$ $/\$
80	78, 79	sylan 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$ $/\$
81		simp2 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$
82	80, 81	syl6bi 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 $/\$
83	82	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
84	83	com23 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
85	77, 84	mpdi 43	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
86	85	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$
87	78	rexrd 9721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
88	87	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
89		elicore 11721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$
90	78, 89	sylan 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$
91	90	rexrd 9721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
92		xrlenlt 9730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$
93	92	biimpd 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$
94	93	con2d 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
95	88, 91, 94	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$
96	86, 95	mt2d 122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$
97	96	intnand 932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
98	97	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$
99	98	con2d 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
100	76, 99	jcad 540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
101		annim 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
102	100, 101	syl6ib 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
103	102	eximdv 1775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
104	74, 103	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
105		exnal 1710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
106	104, 105	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
107		dfss2 3433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
108	106, 107	sylnibr 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
109		imnan 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
110	108, 109	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
111		eleq2 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
112		sseq1 3465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
113	111, 112	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
114	110, 113	mtbiri 309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
115		sseq2 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
116	115	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
117	116	notbid 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
118	114, 117	syl5ibrcom 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
120	119	rexlimivv 2896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
121	71, 120	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
122	121	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
123	122	ralrimiv 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
124		ralnex 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
125	123, 124	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
126	125	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
127	66, 126	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
128	127	adantlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
129	49, 128	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130		an12 811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131		annim 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
132	131	anbi2i 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
133	130, 132	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
134	129, 133	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
135		rspe 2857	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
136	134, 135	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
137		rexnal 2848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
138	136, 137	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
139	138	exp41 619	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
140	139	com4l 87	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
141	140	imp41 602	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
142		rspe 2857	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
143	34, 141, 142	syl2anc 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
144		rexnal 2848	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
145	143, 144	sylib 201	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
146		df-ico 11675	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
147	146	ixxex 11680	. . . . . . . . . . . . . . . . . . . . . . . 24
148		imaexg 6762	. . . . . . . . . . . . . . . . . . . . . . . 24
149	147, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
150	1, 149	eqeltri 2536	. . . . . . . . . . . . . . . . . . . . . 22
151	1	icoreunrn 31808	. . . . . . . . . . . . . . . . . . . . . . 23
152		unirnioo 11768	. . . . . . . . . . . . . . . . . . . . . . 23
153	151, 152	eqtr3i 2486	. . . . . . . . . . . . . . . . . . . . . 22
154		tgss2 20058	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
155	150, 153, 154	mp2an 683	. . . . . . . . . . . . . . . . . . . . 21 $/\$
156	151	raleqi 3003	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
157	155, 156	bitr4i 260	. . . . . . . . . . . . . . . . . . . 20 $/\$
158	145, 157	sylnibr 311	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
159	158	sbcth 3294	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
160	7, 159	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
161		sbcimg 3321	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	7, 161	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	160, 162	mpbi 213	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
164		sbcel1v 3338	. . . . . . . . . . . . . . . . . 18
165	7, 164	mpbir 214	. . . . . . . . . . . . . . . . 17
166		sbcan 3322	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	165, 166	mpbiran2 935	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
168		sbcg 3345	. . . . . . . . . . . . . . . . 17
169	7, 168	ax-mp 5	. . . . . . . . . . . . . . . 16
170	163, 167, 169	3imtr3i 273	. . . . . . . . . . . . . . 15 $/\$ $/\$
171	33, 170	sylbir 218	. . . . . . . . . . . . . 14 $/\$ $/\$
172	21, 32, 171	syl2anbr 487	. . . . . . . . . . . . 13 $/\$ $/\$
173	172	sbcth 3294	. . . . . . . . . . . 12 $/\$ $/\$
174	5, 173	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$
175		sbcimg 3321	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
176	5, 175	ax-mp 5	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
177	174, 176	mpbi 213	. . . . . . . . . 10 $/\$ $/\$
178		sbcan 3322	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179		eqid 2462	. . . . . . . . . . . . 13
180		eqsbc3 3319	. . . . . . . . . . . . . 14
181	5, 180	ax-mp 5	. . . . . . . . . . . . 13
182	179, 181	mpbir 214	. . . . . . . . . . . 12
183		sbcg 3345	. . . . . . . . . . . . . 14 $/\$ $/\$
184	5, 183	ax-mp 5	. . . . . . . . . . . . 13 $/\$ $/\$
185	184	anbi1i 706	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
186	182, 185	mpbiran2 935	. . . . . . . . . . 11 $/\$ $/\$ $/\$
187	178, 186	bitri 257	. . . . . . . . . 10 $/\$ $/\$ $/\$
188		sbcg 3345	. . . . . . . . . . 11
189	5, 188	ax-mp 5	. . . . . . . . . 10
190	177, 187, 189	3imtr3i 273	. . . . . . . . 9 $/\$
191	190	sbcth 3294	. . . . . . . 8 $/\$
192	3, 191	ax-mp 5	. . . . . . 7 $/\$
193		sbcimg 3321	. . . . . . . 8 $/\$ $/\$
194	3, 193	ax-mp 5	. . . . . . 7 $/\$ $/\$
195	192, 194	mpbi 213	. . . . . 6 $/\$
196		sbcan 3322	. . . . . . 7 $/\$ $/\$
197		sbcel1v 3338	. . . . . . . 8
198		sbcbr123 4470	. . . . . . . . 9
199		csbconstg 3388	. . . . . . . . . . 11
200	3, 199	ax-mp 5	. . . . . . . . . 10
201		csbvarg 3804	. . . . . . . . . . 11
202	3, 201	ax-mp 5	. . . . . . . . . 10
203	200, 202	breq12i 4427	. . . . . . . . 9
204		csbconstg 3388	. . . . . . . . . . 11
205	3, 204	ax-mp 5	. . . . . . . . . 10
206	205	breqi 4424	. . . . . . . . 9
207	198, 203, 206	3bitri 279	. . . . . . . 8
208	197, 207	anbi12i 708	. . . . . . 7 $/\$ $/\$
209	196, 208	bitri 257	. . . . . 6 $/\$ $/\$
210		sbcg 3345	. . . . . . 7
211	3, 210	ax-mp 5	. . . . . 6
212	195, 209, 211	3imtr3i 273	. . . . 5 $/\$
213	3, 4, 212	mp2an 683	. . . 4
214		eqimss 3496	. . . 4
215	213, 214	mto 181	. . 3
216	215	nesymir 2694	. 2
217		df-pss 3432	. 2 $/\$
218	2, 216, 217	mpbir2an 936	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wal 1453

wceq 1455

wex 1674

wcel 1898

wne 2633

wral 2749

wrex 2750

crab 2753

cvv 3057

wsbc 3279

csb 3375

wss 3416

wpss 3417

cpw 3963

cop 3986

cuni 4212 class class class wbr 4418

cxp 4854

cdm 4856

crn 4857

cima 4859

wfun 5599

wfn 5600

wf 5601

cfv 5605 (class class class)co 6320

cr 9569

c1 9571

cxr 9705

clt 9706

cle 9707

c2 10692

cioo 11669

cico 11671

ctg 15391

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-fal 1461 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4213 df-iun 4294 df-br 4419 df-opab 4478 df-mpt 4479 df-id 4771 df-po 4777 df-so 4778 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-1st 6825 df-2nd 6826 df-er 7394 df-en 7601 df-dom 7602 df-sdom 7603 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-div 10303 df-2 10701 df-ioo 11673 df-ico 11675 df-topgen 15397

This theorem is referenced by: (None)

W3C validator