difreicc - Metamath Proof Explorer

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

Theorem difreicc 11641

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 3479	. . 3 $\$ $/\$
2		rexr 9628	. . . . . . . . . 10
3		rexr 9628	. . . . . . . . . 10
4		elicc1 11562	. . . . . . . . . 10 $/\$ $/\$ $/\$
5	2, 3, 4	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$
6	5	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	6	notbid 294	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
8		3anass 972	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
9	8	notbii 296	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		ianor 488	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
11		rexr 9628	. . . . . . . . . . . 12
12	11	pm2.24d 143	. . . . . . . . . . 11 $\/$
13	12	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $\/$
14		ianor 488	. . . . . . . . . . 11 $/\$ $\/$
15	11	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
16		mnflt 11322	. . . . . . . . . . . . . . 15
17	16	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		simpr 461	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19		simpll 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		ltnle 9653	. . . . . . . . . . . . . . . . 17 $/\$
21	20	bicomd 201	. . . . . . . . . . . . . . . 16 $/\$
22	18, 19, 21	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	22	biimpa 484	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24		mnfxr 11312	. . . . . . . . . . . . . . 15
25	2	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
26		elioo1 11558	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
27	24, 25, 26	sylancr 663	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
28	15, 17, 23, 27	mpbir3and 1174	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
30		ltnle 9653	. . . . . . . . . . . . . 14 $/\$
31	30	adantll 713	. . . . . . . . . . . . 13 $/\$ $/\$
32	11	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34		ltpnf 11320	. . . . . . . . . . . . . . . 16
35	34	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
36	3	ad3antlr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
37		pnfxr 11310	. . . . . . . . . . . . . . . 16
38		elioo1 11558	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
39	36, 37, 38	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	32, 33, 35, 39	mpbir3and 1174	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
41	40	ex 434	. . . . . . . . . . . . 13 $/\$ $/\$
42	31, 41	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
43	29, 42	orim12d 835	. . . . . . . . . . 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 3638	. . . . 5 $\/$
51	49, 50	syl6ibr 227	. . . 4 $/\$ $/\$
52		ioossre 11575	. . . . . . . . 9
53		ioossre 11575	. . . . . . . . 9
54	52, 53	unssi 3672	. . . . . . . 8
55	54	sseli 3493	. . . . . . 7
56	55	adantl 466	. . . . . 6 $/\$ $/\$
57		elioo2 11559	. . . . . . . . . . . . . . . 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 1205	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	59, 65	sylbid 215	. . . . . . . . . . . . 13 $/\$
67	3	adantl 466	. . . . . . . . . . . . . . 15 $/\$
68	67, 37, 38	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69		xrltnle 9642	. . . . . . . . . . . . . . . . . . . . . 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 1205	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	68, 77	sylbid 215	. . . . . . . . . . . . 13 $/\$
79	66, 78	orim12d 835	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
80	50, 79	syl5bi 217	. . . . . . . . . . 11 $/\$ $\/$
81	80	imp 429	. . . . . . . . . 10 $/\$ $/\$ $\/$
82	81, 14	sylibr 212	. . . . . . . . 9 $/\$ $/\$ $/\$
83	82	intnand 909	. . . . . . . 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 2457	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1374

wcel 1762 $\$ cdif 3466

cun 3467 class class class wbr 4440 (class class class)co 6275

cr 9480

cpnf 9614

cmnf 9615

cxr 9616

clt 9617

cle 9618

cioo 11518

cicc 11521

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-cnex 9537 ax-resscn 9538 ax-pre-lttri 9555 ax-pre-lttrn 9556

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-op 4027 df-uni 4239 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-id 4788 df-po 4793 df-so 4794 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-1st 6774 df-2nd 6775 df-er 7301 df-en 7507 df-dom 7508 df-sdom 7509 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-ioo 11522 df-icc 11525

This theorem is referenced by: icccld 21002 iccmbl 21704 mbfimaicc 21768 icccncfext 31181

W3C validator