difreicc - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > difreicc		Structured version Unicode version

Theorem difreicc 11662

Description: The class difference of

and a closed interval. (Contributed by FL, 18-Jun-2007.)

**Assertion**
Ref	Expression
difreicc	$/\$ $\$

Proof of Theorem difreicc Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldif 3471	. . 3 $\$ $/\$
2		rexr 9642	. . . . . . . . . 10
3		rexr 9642	. . . . . . . . . 10
4		elicc1 11583	. . . . . . . . . 10 $/\$ $/\$ $/\$
5	2, 3, 4	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$
6	5	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	6	notbid 294	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
8		3anass 978	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
9	8	notbii 296	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		ianor 488	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
11		rexr 9642	. . . . . . . . . . . 12
12	11	pm2.24d 143	. . . . . . . . . . 11 $\/$
13	12	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $\/$
14		ianor 488	. . . . . . . . . . 11 $/\$ $\/$
15	11	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
16		mnflt 11343	. . . . . . . . . . . . . . 15
17	16	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		simpr 461	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19		simpll 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		ltnle 9667	. . . . . . . . . . . . . . . . 17 $/\$
21	20	bicomd 201	. . . . . . . . . . . . . . . 16 $/\$
22	18, 19, 21	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	22	biimpa 484	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24		mnfxr 11333	. . . . . . . . . . . . . . 15
25	2	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
26		elioo1 11579	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
27	24, 25, 26	sylancr 663	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
28	15, 17, 23, 27	mpbir3and 1180	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
30		ltnle 9667	. . . . . . . . . . . . . 14 $/\$
31	30	adantll 713	. . . . . . . . . . . . 13 $/\$ $/\$
32	11	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34		ltpnf 11341	. . . . . . . . . . . . . . . 16
35	34	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
36	3	ad3antlr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
37		pnfxr 11331	. . . . . . . . . . . . . . . 16
38		elioo1 11579	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
39	36, 37, 38	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	32, 33, 35, 39	mpbir3and 1180	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
41	40	ex 434	. . . . . . . . . . . . 13 $/\$ $/\$
42	31, 41	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
43	29, 42	orim12d 838	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
44	14, 43	syl5bi 217	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
45	13, 44	jaod 380	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$
46	10, 45	syl5bi 217	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$
47	9, 46	syl5bi 217	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$
48	7, 47	sylbid 215	. . . . . 6 $/\$ $/\$ $\/$
49	48	expimpd 603	. . . . 5 $/\$ $/\$ $\/$
50		elun 3630	. . . . 5 $\/$
51	49, 50	syl6ibr 227	. . . 4 $/\$ $/\$
52		ioossre 11596	. . . . . . . . 9
53		ioossre 11596	. . . . . . . . 9
54	52, 53	unssi 3664	. . . . . . . 8
55	54	sseli 3485	. . . . . . 7
56	55	adantl 466	. . . . . 6 $/\$ $/\$
57		elioo2 11580	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
58	24, 2, 57	sylancr 663	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	58	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
60	20	biimpd 207	. . . . . . . . . . . . . . . . . . 19 $/\$
61	60	ex 434	. . . . . . . . . . . . . . . . . 18
62	61	a1i 11	. . . . . . . . . . . . . . . . 17
63	62	com13 80	. . . . . . . . . . . . . . . 16
64	63	adantr 465	. . . . . . . . . . . . . . 15 $/\$
65	64	3impd 1211	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	59, 65	sylbid 215	. . . . . . . . . . . . 13 $/\$
67	3	adantl 466	. . . . . . . . . . . . . . 15 $/\$
68	67, 37, 38	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69		xrltnle 9656	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
70	69	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 $/\$
71	70	ex 434	. . . . . . . . . . . . . . . . . . . 20
72	71	com3l 81	. . . . . . . . . . . . . . . . . . 19
73	72	a1i 11	. . . . . . . . . . . . . . . . . 18
74	73	com14 88	. . . . . . . . . . . . . . . . 17
75	3, 74	syl 16	. . . . . . . . . . . . . . . 16
76	75	adantl 466	. . . . . . . . . . . . . . 15 $/\$
77	76	3impd 1211	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	68, 77	sylbid 215	. . . . . . . . . . . . 13 $/\$
79	66, 78	orim12d 838	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
80	50, 79	syl5bi 217	. . . . . . . . . . 11 $/\$ $\/$
81	80	imp 429	. . . . . . . . . 10 $/\$ $/\$ $\/$
82	81, 14	sylibr 212	. . . . . . . . 9 $/\$ $/\$ $/\$
83	82	intnand 916	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
84	83, 8	sylnibr 305	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
85	2, 3	anim12i 566	. . . . . . . . 9 $/\$ $/\$
86	85	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$
87	4	notbid 294	. . . . . . . 8 $/\$ $/\$ $/\$
88	86, 87	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89	84, 88	mpbird 232	. . . . . 6 $/\$ $/\$
90	56, 89	jca 532	. . . . 5 $/\$ $/\$ $/\$
91	90	ex 434	. . . 4 $/\$ $/\$
92	51, 91	impbid 191	. . 3 $/\$ $/\$
93	1, 92	syl5bb 257	. 2 $/\$ $\$
94	93	eqrdv 2440	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 974

wceq 1383

wcel 1804 $\$ cdif 3458

cun 3459 class class class wbr 4437 (class class class)co 6281

cr 9494

cpnf 9628

cmnf 9629

cxr 9630

clt 9631

cle 9632

cioo 11539

cicc 11542

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-pre-lttri 9569 ax-pre-lttrn 9570

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-id 4785 df-po 4790 df-so 4791 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-1st 6785 df-2nd 6786 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-ioo 11543 df-icc 11546

This theorem is referenced by: icccld 21251 iccmbl 21953 mbfimaicc 22017 icccncfext 31597

W3C validator