difreicc - Metamath Proof Explorer

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

Theorem difreicc 11621

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 3421	. . 3 $\$ $/\$
2		rexr 9587	. . . . . . . . . 10
3		rexr 9587	. . . . . . . . . 10
4		elicc1 11542	. . . . . . . . . 10 $/\$ $/\$ $/\$
5	2, 3, 4	syl2an 475	. . . . . . . . 9 $/\$ $/\$ $/\$
6	5	adantr 463	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
7	6	notbid 292	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
8		3anass 976	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
9	8	notbii 294	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
10		ianor 486	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
11		rexr 9587	. . . . . . . . . . . 12
12	11	pm2.24d 143	. . . . . . . . . . 11 $\/$
13	12	adantl 464	. . . . . . . . . 10 $/\$ $/\$ $\/$
14		ianor 486	. . . . . . . . . . 11 $/\$ $\/$
15	11	ad2antlr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
16		mnflt 11302	. . . . . . . . . . . . . . 15
17	16	ad2antlr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		simpr 459	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19		simpll 752	. . . . . . . . . . . . . . . 16 $/\$ $/\$
20		ltnle 9613	. . . . . . . . . . . . . . . . 17 $/\$
21	20	bicomd 201	. . . . . . . . . . . . . . . 16 $/\$
22	18, 19, 21	syl2anc 659	. . . . . . . . . . . . . . 15 $/\$ $/\$
23	22	biimpa 482	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24		mnfxr 11292	. . . . . . . . . . . . . . 15
25	2	ad3antrrr 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
26		elioo1 11538	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
27	24, 25, 26	sylancr 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
28	15, 17, 23, 27	mpbir3and 1178	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	ex 432	. . . . . . . . . . . 12 $/\$ $/\$
30		ltnle 9613	. . . . . . . . . . . . . 14 $/\$
31	30	adantll 712	. . . . . . . . . . . . 13 $/\$ $/\$
32	11	ad2antlr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		simpr 459	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34		ltpnf 11300	. . . . . . . . . . . . . . . 16
35	34	ad2antlr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
36	3	ad3antlr 729	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
37		pnfxr 11290	. . . . . . . . . . . . . . . 16
38		elioo1 11538	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
39	36, 37, 38	sylancl 660	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
40	32, 33, 35, 39	mpbir3and 1178	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
41	40	ex 432	. . . . . . . . . . . . 13 $/\$ $/\$
42	31, 41	sylbird 235	. . . . . . . . . . . 12 $/\$ $/\$
43	29, 42	orim12d 837	. . . . . . . . . . 11 $/\$ $/\$ $\/$ $\/$
44	14, 43	syl5bi 217	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\/$
45	13, 44	jaod 378	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$
46	10, 45	syl5bi 217	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$
47	9, 46	syl5bi 217	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$
48	7, 47	sylbid 215	. . . . . 6 $/\$ $/\$ $\/$
49	48	expimpd 601	. . . . 5 $/\$ $/\$ $\/$
50		elun 3581	. . . . 5 $\/$
51	49, 50	syl6ibr 227	. . . 4 $/\$ $/\$
52		ioossre 11555	. . . . . . . . 9
53		ioossre 11555	. . . . . . . . 9
54	52, 53	unssi 3615	. . . . . . . 8
55	54	sseli 3435	. . . . . . 7
56	55	adantl 464	. . . . . 6 $/\$ $/\$
57		elioo2 11539	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
58	24, 2, 57	sylancr 661	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	58	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
60	20	biimpd 207	. . . . . . . . . . . . . . . . . . 19 $/\$
61	60	ex 432	. . . . . . . . . . . . . . . . . 18
62	61	a1i 11	. . . . . . . . . . . . . . . . 17
63	62	com13 80	. . . . . . . . . . . . . . . 16
64	63	adantr 463	. . . . . . . . . . . . . . 15 $/\$
65	64	3impd 1209	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	59, 65	sylbid 215	. . . . . . . . . . . . 13 $/\$
67	3	adantl 464	. . . . . . . . . . . . . . 15 $/\$
68	67, 37, 38	sylancl 660	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69		xrltnle 9601	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
70	69	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 $/\$
71	70	ex 432	. . . . . . . . . . . . . . . . . . . 20
72	71	com3l 81	. . . . . . . . . . . . . . . . . . 19
73	72	a1i 11	. . . . . . . . . . . . . . . . . 18
74	73	com14 88	. . . . . . . . . . . . . . . . 17
75	3, 74	syl 17	. . . . . . . . . . . . . . . 16
76	75	adantl 464	. . . . . . . . . . . . . . 15 $/\$
77	76	3impd 1209	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
78	68, 77	sylbid 215	. . . . . . . . . . . . 13 $/\$
79	66, 78	orim12d 837	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
80	50, 79	syl5bi 217	. . . . . . . . . . 11 $/\$ $\/$
81	80	imp 427	. . . . . . . . . 10 $/\$ $/\$ $\/$
82	81, 14	sylibr 212	. . . . . . . . 9 $/\$ $/\$ $/\$
83	82	intnand 915	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
84	83, 8	sylnibr 303	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
85	2, 3	anim12i 564	. . . . . . . . 9 $/\$ $/\$
86	85	adantr 463	. . . . . . . 8 $/\$ $/\$ $/\$
87	4	notbid 292	. . . . . . . 8 $/\$ $/\$ $/\$
88	86, 87	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89	84, 88	mpbird 232	. . . . . 6 $/\$ $/\$
90	56, 89	jca 530	. . . . 5 $/\$ $/\$ $/\$
91	90	ex 432	. . . 4 $/\$ $/\$
92	51, 91	impbid 191	. . 3 $/\$ $/\$
93	1, 92	syl5bb 257	. 2 $/\$ $\$
94	93	eqrdv 2397	1 $/\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 972

wceq 1403

wcel 1840 $\$ cdif 3408

cun 3409 class class class wbr 4392 (class class class)co 6232

cr 9439

cpnf 9573

cmnf 9574

cxr 9575

clt 9576

cle 9577

cioo 11498

cicc 11501

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1637 ax-4 1650 ax-5 1723 ax-6 1769 ax-7 1812 ax-8 1842 ax-9 1844 ax-10 1859 ax-11 1864 ax-12 1876 ax-13 2024 ax-ext 2378 ax-sep 4514 ax-nul 4522 ax-pow 4569 ax-pr 4627 ax-un 6528 ax-cnex 9496 ax-resscn 9497 ax-pre-lttri 9514 ax-pre-lttrn 9515

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 973 df-3an 974 df-tru 1406 df-ex 1632 df-nf 1636 df-sb 1762 df-eu 2240 df-mo 2241 df-clab 2386 df-cleq 2392 df-clel 2395 df-nfc 2550 df-ne 2598 df-nel 2599 df-ral 2756 df-rex 2757 df-rab 2760 df-v 3058 df-sbc 3275 df-csb 3371 df-dif 3414 df-un 3416 df-in 3418 df-ss 3425 df-nul 3736 df-if 3883 df-pw 3954 df-sn 3970 df-pr 3972 df-op 3976 df-uni 4189 df-iun 4270 df-br 4393 df-opab 4451 df-mpt 4452 df-id 4735 df-po 4741 df-so 4742 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5487 df-fun 5525 df-fn 5526 df-f 5527 df-f1 5528 df-fo 5529 df-f1o 5530 df-fv 5531 df-ov 6235 df-oprab 6236 df-mpt2 6237 df-1st 6736 df-2nd 6737 df-er 7266 df-en 7473 df-dom 7474 df-sdom 7475 df-pnf 9578 df-mnf 9579 df-xr 9580 df-ltxr 9581 df-le 9582 df-ioo 11502 df-icc 11505

This theorem is referenced by: icccld 21456 iccmbl 22158 mbfimaicc 22222 icccncfext 37025

W3C validator