difreicc - Metamath Proof Explorer

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

Theorem difreicc 11799

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 3426	. . 3 $\$ $/\$
2		rexr 9717	. . . . . . . . . 10
3		rexr 9717	. . . . . . . . . 10
4		elicc1 11714	. . . . . . . . . 10 $/\$ $/\$ $/\$
5	2, 3, 4	syl2an 484	. . . . . . . . 9 $/\$ $/\$ $/\$
6	5	adantr 471	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	6	notbid 300	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
8		3anass 995	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
9	8	notbii 302	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		ianor 495	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
11		rexr 9717	. . . . . . . . . . . 12
12	11	pm2.24d 139	. . . . . . . . . . 11 $\/$
13	12	adantl 472	. . . . . . . . . 10 $/\$ $/\$ $\/$
14		ianor 495	. . . . . . . . . . 11 $/\$ $\/$
15	11	ad2antlr 738	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
16		mnflt 11459	. . . . . . . . . . . . . . 15
17	16	ad2antlr 738	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		simpr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19		simpll 765	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		ltnle 9744	. . . . . . . . . . . . . . . . 17 $/\$
21	20	bicomd 206	. . . . . . . . . . . . . . . 16 $/\$
22	18, 19, 21	syl2anc 671	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	22	biimpa 491	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24		mnfxr 11448	. . . . . . . . . . . . . . 15
25	2	ad3antrrr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
26		elioo1 11710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
27	24, 25, 26	sylancr 674	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
28	15, 17, 23, 27	mpbir3and 1197	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	ex 440	. . . . . . . . . . . 12 $/\$ $/\$
30		ltnle 9744	. . . . . . . . . . . . . 14 $/\$
31	30	adantll 725	. . . . . . . . . . . . 13 $/\$ $/\$
32	11	ad2antlr 738	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		simpr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34		ltpnf 11456	. . . . . . . . . . . . . . . 16
35	34	ad2antlr 738	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
36	3	ad3antlr 742	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
37		pnfxr 11446	. . . . . . . . . . . . . . . 16
38		elioo1 11710	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
39	36, 37, 38	sylancl 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	32, 33, 35, 39	mpbir3and 1197	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
41	40	ex 440	. . . . . . . . . . . . 13 $/\$ $/\$
42	31, 41	sylbird 243	. . . . . . . . . . . 12 $/\$ $/\$
43	29, 42	orim12d 854	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
44	14, 43	syl5bi 225	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
45	13, 44	jaod 386	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$
46	10, 45	syl5bi 225	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$
47	9, 46	syl5bi 225	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$
48	7, 47	sylbid 223	. . . . . 6 $/\$ $/\$ $\/$
49	48	expimpd 612	. . . . 5 $/\$ $/\$ $\/$
50		elun 3586	. . . . 5 $\/$
51	49, 50	syl6ibr 235	. . . 4 $/\$ $/\$
52		ioossre 11730	. . . . . . . . 9
53		ioossre 11730	. . . . . . . . 9
54	52, 53	unssi 3621	. . . . . . . 8
55	54	sseli 3440	. . . . . . 7
56	55	adantl 472	. . . . . 6 $/\$ $/\$
57		elioo2 11711	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
58	24, 2, 57	sylancr 674	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	58	adantr 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
60	20	biimpd 212	. . . . . . . . . . . . . . . . . . 19 $/\$
61	60	ex 440	. . . . . . . . . . . . . . . . . 18
62	61	a1i 11	. . . . . . . . . . . . . . . . 17
63	62	com13 83	. . . . . . . . . . . . . . . 16
64	63	adantr 471	. . . . . . . . . . . . . . 15 $/\$
65	64	3impd 1231	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	59, 65	sylbid 223	. . . . . . . . . . . . 13 $/\$
67	3	adantl 472	. . . . . . . . . . . . . . 15 $/\$
68	67, 37, 38	sylancl 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69		xrltnle 9732	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
70	69	biimpd 212	. . . . . . . . . . . . . . . . . . . . 21 $/\$
71	70	ex 440	. . . . . . . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . 15 $/\$
77	76	3impd 1231	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	68, 77	sylbid 223	. . . . . . . . . . . . 13 $/\$
79	66, 78	orim12d 854	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
80	50, 79	syl5bi 225	. . . . . . . . . . 11 $/\$ $\/$
81	80	imp 435	. . . . . . . . . 10 $/\$ $/\$ $\/$
82	81, 14	sylibr 217	. . . . . . . . 9 $/\$ $/\$ $/\$
83	82	intnand 932	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
84	83, 8	sylnibr 311	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
85	2, 3	anim12i 574	. . . . . . . . 9 $/\$ $/\$
86	85	adantr 471	. . . . . . . 8 $/\$ $/\$ $/\$
87	4	notbid 300	. . . . . . . 8 $/\$ $/\$ $/\$
88	86, 87	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89	84, 88	mpbird 240	. . . . . 6 $/\$ $/\$
90	56, 89	jca 539	. . . . 5 $/\$ $/\$ $/\$
91	90	ex 440	. . . 4 $/\$ $/\$
92	51, 91	impbid 195	. . 3 $/\$ $/\$
93	1, 92	syl5bb 265	. 2 $/\$ $\$
94	93	eqrdv 2460	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1455

wcel 1898 $\$ cdif 3413

cun 3414 class class class wbr 4418 (class class class)co 6320

cr 9569

cpnf 9703

cmnf 9704

cxr 9705

clt 9706

cle 9707

cioo 11669

cicc 11672

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-pre-lttri 9644 ax-pre-lttrn 9645

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 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-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 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-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-ioo 11673 df-icc 11676

This theorem is referenced by: icccld 21842 iccmbl 22575 mbfimaicc 22645 icccncfext 37851

W3C validator