difreicc - Metamath Proof Explorer

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

Theorem difreicc 11415

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 3336	. . 3 $\$ $/\$
2		rexr 9427	. . . . . . . . . 10
3		rexr 9427	. . . . . . . . . 10
4		elicc1 11342	. . . . . . . . . 10 $/\$ $/\$ $/\$
5	2, 3, 4	syl2an 477	. . . . . . . . 9 $/\$ $/\$ $/\$
6	5	adantr 465	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	6	notbid 294	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
8		3anass 969	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
9	8	notbii 296	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		ianor 488	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
11		rexr 9427	. . . . . . . . . . . 12
12	11	pm2.24d 143	. . . . . . . . . . 11 $\/$
13	12	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $\/$
14		ianor 488	. . . . . . . . . . 11 $/\$ $\/$
15	11	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
16		mnflt 11102	. . . . . . . . . . . . . . 15
17	16	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		simpr 461	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19		simpll 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		ltnle 9452	. . . . . . . . . . . . . . . . 17 $/\$
21	20	bicomd 201	. . . . . . . . . . . . . . . 16 $/\$
22	18, 19, 21	syl2anc 661	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	22	biimpa 484	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24		mnfxr 11092	. . . . . . . . . . . . . . 15
25	2	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
26		elioo1 11338	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
27	24, 25, 26	sylancr 663	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
28	15, 17, 23, 27	mpbir3and 1171	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	ex 434	. . . . . . . . . . . 12 $/\$ $/\$
30		ltnle 9452	. . . . . . . . . . . . . 14 $/\$
31	30	adantll 713	. . . . . . . . . . . . 13 $/\$ $/\$
32	11	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34		ltpnf 11100	. . . . . . . . . . . . . . . 16
35	34	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
36	3	ad3antlr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
37		pnfxr 11090	. . . . . . . . . . . . . . . 16
38		elioo1 11338	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
39	36, 37, 38	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	32, 33, 35, 39	mpbir3and 1171	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
41	40	ex 434	. . . . . . . . . . . . 13 $/\$ $/\$
42	31, 41	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
43	29, 42	orim12d 834	. . . . . . . . . . 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 3495	. . . . 5 $\/$
51	49, 50	syl6ibr 227	. . . 4 $/\$ $/\$
52		ioossre 11355	. . . . . . . . 9
53		ioossre 11355	. . . . . . . . 9
54	52, 53	unssi 3529	. . . . . . . 8
55	54	sseli 3350	. . . . . . 7
56	55	adantl 466	. . . . . 6 $/\$ $/\$
57		elioo2 11339	. . . . . . . . . . . . . . . 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 1201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	59, 65	sylbid 215	. . . . . . . . . . . . 13 $/\$
67	3	adantl 466	. . . . . . . . . . . . . . 15 $/\$
68	67, 37, 38	sylancl 662	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69		xrltnle 9441	. . . . . . . . . . . . . . . . . . . . . 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 1201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	68, 77	sylbid 215	. . . . . . . . . . . . 13 $/\$
79	66, 78	orim12d 834	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
80	50, 79	syl5bi 217	. . . . . . . . . . 11 $/\$ $\/$
81	80	imp 429	. . . . . . . . . 10 $/\$ $/\$ $\/$
82	81, 14	sylibr 212	. . . . . . . . 9 $/\$ $/\$ $/\$
83	82	intnand 907	. . . . . . . 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 2439	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756 $\$ cdif 3323

cun 3324 class class class wbr 4290 (class class class)co 6089

cr 9279

cpnf 9413

cmnf 9414

cxr 9415

clt 9416

cle 9417

cioo 11298

cicc 11301

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2422 ax-sep 4411 ax-nul 4419 ax-pow 4468 ax-pr 4529 ax-un 6370 ax-cnex 9336 ax-resscn 9337 ax-pre-lttri 9354 ax-pre-lttrn 9355

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-rab 2722 df-v 2972 df-sbc 3185 df-csb 3287 df-dif 3329 df-un 3331 df-in 3333 df-ss 3340 df-nul 3636 df-if 3790 df-pw 3860 df-sn 3876 df-pr 3878 df-op 3882 df-uni 4090 df-iun 4171 df-br 4291 df-opab 4349 df-mpt 4350 df-id 4634 df-po 4639 df-so 4640 df-xp 4844 df-rel 4845 df-cnv 4846 df-co 4847 df-dm 4848 df-rn 4849 df-res 4850 df-ima 4851 df-iota 5379 df-fun 5418 df-fn 5419 df-f 5420 df-f1 5421 df-fo 5422 df-f1o 5423 df-fv 5424 df-ov 6092 df-oprab 6093 df-mpt2 6094 df-1st 6575 df-2nd 6576 df-er 7099 df-en 7309 df-dom 7310 df-sdom 7311 df-pnf 9418 df-mnf 9419 df-xr 9420 df-ltxr 9421 df-le 9422 df-ioo 11302 df-icc 11305

This theorem is referenced by: icccld 20344 iccmbl 21045 mbfimaicc 21109

W3C validator