Theorem cdrci 10494

Description: The class difference of RR and a closed interval.

Assertion

Ref	Expression
cdrci	|- ((A e. RR /\ B e. RR) -> (RR \ (A[,]B)) = U.{( -oo(,)A), (B(,) +oo)})

Proof of Theorem cdrci

Step	Hyp	Ref	Expression
1		elicc1t 6383	. . . . . . . . . . . 12 |- ((A e. RR* /\ B e. RR*) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ x /\ x <_ B)))
2		rexrt 5499	. . . . . . . . . . . 12 |- (A e. RR -> A e. RR*)
3		rexrt 5499	. . . . . . . . . . . 12 |- (B e. RR -> B e. RR*)
4	1, 2, 3	syl2an 454	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ x /\ x <_ B)))
5	4	adantr 389	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ x /\ x <_ B)))
6	5	negbid 611	. . . . . . . . 9 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. x e. (A[,]B) <-> -. (x e. RR* /\ A <_ x /\ x <_ B)))
7		rexrt 5499	. . . . . . . . . . . . . 14 |- (x e. RR -> x e. RR*)
8	7	pm2.24d 105	. . . . . . . . . . . . 13 |- (x e. RR -> (-. x e. RR* -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
9	8	adantl 388	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. x e. RR* -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
10	7	ad2antlr 405	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> x e. RR*)
11		mnfltt 5543	. . . . . . . . . . . . . . . . . 18 |- (x e. RR -> -oo < x)
12	11	ad2antlr 405	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> -oo < x)
13		ltnlet 5511	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. RR /\ A e. RR) -> (x < A <-> -. A <_ x))
14	13	bicomd 521	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ A e. RR) -> (-. A <_ x <-> x < A))
15		pm3.27 323	. . . . . . . . . . . . . . . . . . 19 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> x e. RR)
16		simpll 412	. . . . . . . . . . . . . . . . . . 19 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> A e. RR)
17	14, 15, 16	sylanc 471	. . . . . . . . . . . . . . . . . 18 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. A <_ x <-> x < A))
18	17	biimpa 416	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> x < A)
19	10, 12, 18	3jca 819	. . . . . . . . . . . . . . . 16 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> (x e. RR* /\ -oo < x /\ x < A))
20	2	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ B e. RR) -> A e. RR*)
21	20	ad2antrr 404	. . . . . . . . . . . . . . . . . 18 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> A e. RR*)
22		mnfxr 5494	. . . . . . . . . . . . . . . . . 18 |- -oo e. RR*
23	21, 22	jctil 292	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> ( -oo e. RR* /\ A e. RR*))
24		elioo1t 6378	. . . . . . . . . . . . . . . . 17 |- (( -oo e. RR* /\ A e. RR*) -> (x e. ( -oo(,)A) <-> (x e. RR* /\ -oo < x /\ x < A)))
25	23, 24	syl 10	. . . . . . . . . . . . . . . 16 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> (x e. ( -oo(,)A) <-> (x e. RR* /\ -oo < x /\ x < A)))
26	19, 25	mpbird 196	. . . . . . . . . . . . . . 15 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ -. A <_ x) -> x e. ( -oo(,)A))
27	26	ex 373	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. A <_ x -> x e. ( -oo(,)A)))
28		ltnlet 5511	. . . . . . . . . . . . . . . 16 |- ((B e. RR /\ x e. RR) -> (B < x <-> -. x <_ B))
29	28	adantll 392	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (B < x <-> -. x <_ B))
30	7	ad2antlr 405	. . . . . . . . . . . . . . . . . 18 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> x e. RR*)
31		pm3.27 323	. . . . . . . . . . . . . . . . . 18 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> B < x)
32		ltpnft 5542	. . . . . . . . . . . . . . . . . . 19 |- (x e. RR -> x < +oo)
33	32	ad2antlr 405	. . . . . . . . . . . . . . . . . 18 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> x < +oo)
34	30, 31, 33	3jca 819	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> (x e. RR* /\ B < x /\ x < +oo))
35	3	adantl 388	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. RR /\ B e. RR) -> B e. RR*)
36	35	ad2antrr 404	. . . . . . . . . . . . . . . . . . 19 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> B e. RR*)
37		pnfxr 5493	. . . . . . . . . . . . . . . . . . 19 |- +oo e. RR*
38	36, 37	jctir 293	. . . . . . . . . . . . . . . . . 18 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> (B e. RR* /\ +oo e. RR*))
39		elioo1t 6378	. . . . . . . . . . . . . . . . . 18 |- ((B e. RR* /\ +oo e. RR*) -> (x e. (B(,) +oo) <-> (x e. RR* /\ B < x /\ x < +oo)))
40	38, 39	syl 10	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> (x e. (B(,) +oo) <-> (x e. RR* /\ B < x /\ x < +oo)))
41	34, 40	mpbird 196	. . . . . . . . . . . . . . . 16 |- ((((A e. RR /\ B e. RR) /\ x e. RR) /\ B < x) -> x e. (B(,) +oo))
42	41	ex 373	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (B < x -> x e. (B(,) +oo)))
43	29, 42	sylbird 205	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. x <_ B -> x e. (B(,) +oo)))
44	27, 43	orim12d 565	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> ((-. A <_ x \/ -. x <_ B) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
45		ianor 305	. . . . . . . . . . . . 13 |- (-. (A <_ x /\ x <_ B) <-> (-. A <_ x \/ -. x <_ B))
46	44, 45	syl5ib 206	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. (A <_ x /\ x <_ B) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
47	9, 46	jaod 424	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> ((-. x e. RR* \/ -. (A <_ x /\ x <_ B)) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
48		ianor 305	. . . . . . . . . . 11 |- (-. (x e. RR* /\ (A <_ x /\ x <_ B)) <-> (-. x e. RR* \/ -. (A <_ x /\ x <_ B)))
49	47, 48	syl5ib 206	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. (x e. RR* /\ (A <_ x /\ x <_ B)) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
50		3anass 779	. . . . . . . . . . 11 |- ((x e. RR* /\ A <_ x /\ x <_ B) <-> (x e. RR* /\ (A <_ x /\ x <_ B)))
51	50	negbii 187	. . . . . . . . . 10 |- (-. (x e. RR* /\ A <_ x /\ x <_ B) <-> -. (x e. RR* /\ (A <_ x /\ x <_ B)))
52	49, 51	syl5ib 206	. . . . . . . . 9 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. (x e. RR* /\ A <_ x /\ x <_ B) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
53	6, 52	sylbid 203	. . . . . . . 8 |- (((A e. RR /\ B e. RR) /\ x e. RR) -> (-. x e. (A[,]B) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
54	53	ex 373	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (x e. RR -> (-. x e. (A[,]B) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo)))))
55	54	imp3a 361	. . . . . 6 |- ((A e. RR /\ B e. RR) -> ((x e. RR /\ -. x e. (A[,]B)) -> (x e. ( -oo(,)A) \/ x e. (B(,) +oo))))
56		elun 2173	. . . . . 6 |- (x e. (( -oo(,)A) u. (B(,) +oo)) <-> (x e. ( -oo(,)A) \/ x e. (B(,) +oo)))
57	55, 56	syl6ibr 213	. . . . 5 |- ((A e. RR /\ B e. RR) -> ((x e. RR /\ -. x e. (A[,]B)) -> x e. (( -oo(,)A) u. (B(,) +oo))))
58		ioossre 6389	. . . . . . . . . 10 |- ( -oo(,)A) (_ RR
59		ioossre 6389	. . . . . . . . . 10 |- (B(,) +oo) (_ RR
60	58, 59	unssi 2205	. . . . . . . . 9 |- (( -oo(,)A) u. (B(,) +oo)) (_ RR
61	60	sseli 2065	. . . . . . . 8 |- (x e. (( -oo(,)A) u. (B(,) +oo)) -> x e. RR)
62	61	adantl 388	. . . . . . 7 |- (((A e. RR /\ B e. RR) /\ x e. (( -oo(,)A) u. (B(,) +oo))) -> x e. RR)
63		elioo2t 6379	. . . . . . . . . . . . . . . . . . 19 |- (( -oo e. RR* /\ A e. RR*) -> (x e. ( -oo(,)A) <-> (x e. RR /\ -oo < x /\ x < A)))
64	63	ex 373	. . . . . . . . . . . . . . . . . 18 |- ( -oo e. RR* -> (A e. RR* -> (x e. ( -oo(,)A) <-> (x e. RR /\ -oo < x /\ x < A))))
65	64, 2