difreicc - Metamath Proof Explorer

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

Theorem difreicc 11771

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 3446	. . 3 $\$ $/\$
2		rexr 9693	. . . . . . . . . 10
3		rexr 9693	. . . . . . . . . 10
4		elicc1 11687	. . . . . . . . . 10 $/\$ $/\$ $/\$
5	2, 3, 4	syl2an 479	. . . . . . . . 9 $/\$ $/\$ $/\$
6	5	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	6	notbid 295	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
8		3anass 986	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
9	8	notbii 297	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		ianor 490	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
11		rexr 9693	. . . . . . . . . . . 12
12	11	pm2.24d 137	. . . . . . . . . . 11 $\/$
13	12	adantl 467	. . . . . . . . . 10 $/\$ $/\$ $\/$
14		ianor 490	. . . . . . . . . . 11 $/\$ $\/$
15	11	ad2antlr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
16		mnflt 11432	. . . . . . . . . . . . . . 15
17	16	ad2antlr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		simpr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19		simpll 758	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		ltnle 9720	. . . . . . . . . . . . . . . . 17 $/\$
21	20	bicomd 204	. . . . . . . . . . . . . . . 16 $/\$
22	18, 19, 21	syl2anc 665	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	22	biimpa 486	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24		mnfxr 11421	. . . . . . . . . . . . . . 15
25	2	ad3antrrr 734	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
26		elioo1 11683	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
27	24, 25, 26	sylancr 667	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
28	15, 17, 23, 27	mpbir3and 1188	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	ex 435	. . . . . . . . . . . 12 $/\$ $/\$
30		ltnle 9720	. . . . . . . . . . . . . 14 $/\$
31	30	adantll 718	. . . . . . . . . . . . 13 $/\$ $/\$
32	11	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		simpr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34		ltpnf 11429	. . . . . . . . . . . . . . . 16
35	34	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
36	3	ad3antlr 735	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
37		pnfxr 11419	. . . . . . . . . . . . . . . 16
38		elioo1 11683	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
39	36, 37, 38	sylancl 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	32, 33, 35, 39	mpbir3and 1188	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
41	40	ex 435	. . . . . . . . . . . . 13 $/\$ $/\$
42	31, 41	sylbird 238	. . . . . . . . . . . 12 $/\$ $/\$
43	29, 42	orim12d 846	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
44	14, 43	syl5bi 220	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
45	13, 44	jaod 381	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$
46	10, 45	syl5bi 220	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$
47	9, 46	syl5bi 220	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$
48	7, 47	sylbid 218	. . . . . 6 $/\$ $/\$ $\/$
49	48	expimpd 606	. . . . 5 $/\$ $/\$ $\/$
50		elun 3606	. . . . 5 $\/$
51	49, 50	syl6ibr 230	. . . 4 $/\$ $/\$
52		ioossre 11703	. . . . . . . . 9
53		ioossre 11703	. . . . . . . . 9
54	52, 53	unssi 3641	. . . . . . . 8
55	54	sseli 3460	. . . . . . 7
56	55	adantl 467	. . . . . 6 $/\$ $/\$
57		elioo2 11684	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
58	24, 2, 57	sylancr 667	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	58	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
60	20	biimpd 210	. . . . . . . . . . . . . . . . . . 19 $/\$
61	60	ex 435	. . . . . . . . . . . . . . . . . 18
62	61	a1i 11	. . . . . . . . . . . . . . . . 17
63	62	com13 83	. . . . . . . . . . . . . . . 16
64	63	adantr 466	. . . . . . . . . . . . . . 15 $/\$
65	64	3impd 1219	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	59, 65	sylbid 218	. . . . . . . . . . . . 13 $/\$
67	3	adantl 467	. . . . . . . . . . . . . . 15 $/\$
68	67, 37, 38	sylancl 666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69		xrltnle 9708	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
70	69	biimpd 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$
71	70	ex 435	. . . . . . . . . . . . . . . . . . . 20
72	71	com3l 84	. . . . . . . . . . . . . . . . . . 19
73	72	a1i 11	. . . . . . . . . . . . . . . . . 18
74	73	com14 91	. . . . . . . . . . . . . . . . 17
75	3, 74	syl 17	. . . . . . . . . . . . . . . 16
76	75	adantl 467	. . . . . . . . . . . . . . 15 $/\$
77	76	3impd 1219	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	68, 77	sylbid 218	. . . . . . . . . . . . 13 $/\$
79	66, 78	orim12d 846	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
80	50, 79	syl5bi 220	. . . . . . . . . . 11 $/\$ $\/$
81	80	imp 430	. . . . . . . . . 10 $/\$ $/\$ $\/$
82	81, 14	sylibr 215	. . . . . . . . 9 $/\$ $/\$ $/\$
83	82	intnand 924	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
84	83, 8	sylnibr 306	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
85	2, 3	anim12i 568	. . . . . . . . 9 $/\$ $/\$
86	85	adantr 466	. . . . . . . 8 $/\$ $/\$ $/\$
87	4	notbid 295	. . . . . . . 8 $/\$ $/\$ $/\$
88	86, 87	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89	84, 88	mpbird 235	. . . . . 6 $/\$ $/\$
90	56, 89	jca 534	. . . . 5 $/\$ $/\$ $/\$
91	90	ex 435	. . . 4 $/\$ $/\$
92	51, 91	impbid 193	. . 3 $/\$ $/\$
93	1, 92	syl5bb 260	. 2 $/\$ $\$
94	93	eqrdv 2419	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872 $\$ cdif 3433

cun 3434 class class class wbr 4423 (class class class)co 6305

cr 9545

cpnf 9679

cmnf 9680

cxr 9681

clt 9682

cle 9683

cioo 11642

cicc 11645

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597 ax-cnex 9602 ax-resscn 9603 ax-pre-lttri 9620 ax-pre-lttrn 9621

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4220 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-id 4768 df-po 4774 df-so 4775 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-1st 6807 df-2nd 6808 df-er 7374 df-en 7581 df-dom 7582 df-sdom 7583 df-pnf 9684 df-mnf 9685 df-xr 9686 df-ltxr 9687 df-le 9688 df-ioo 11646 df-icc 11649

This theorem is referenced by: icccld 21785 iccmbl 22517 mbfimaicc 22587 icccncfext 37705

W3C validator