Theorem ioojoint 6417

Description: Join two open intervals to create a third.

Assertion

Ref	Expression
ioojoint	|- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) -> (((A(,)B) u. {B}) u. (B(,)C)) = (A(,)C))

Proof of Theorem ioojoint

Step	Hyp	Ref	Expression
1		snunioo 6416	. . . . . . 7 |- ((B e. RR /\ C e. RR /\ B < C) -> ({B} u. (B(,)C)) = (B[,)C))
2	1	3expa 835	. . . . . 6 |- (((B e. RR /\ C e. RR) /\ B < C) -> ({B} u. (B(,)C)) = (B[,)C))
3	2	3adantl1 805	. . . . 5 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ B < C) -> ({B} u. (B(,)C)) = (B[,)C))
4	3	adantrl 396	. . . 4 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) -> ({B} u. (B(,)C)) = (B[,)C))
5	4	uneq2d 2187	. . 3 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) -> ((A(,)B) u. ({B} u. (B(,)C))) = ((A(,)B) u. (B[,)C)))
6		elioo2t 6380	. . . . . . . . . . . 12 |- ((A e. RR* /\ B e. RR*) -> (x e. (A(,)B) <-> (x e. RR /\ A < x /\ x < B)))
7		rexrt 5511	. . . . . . . . . . . 12 |- (A e. RR -> A e. RR*)
8		rexrt 5511	. . . . . . . . . . . 12 |- (B e. RR -> B e. RR*)
9	6, 7, 8	syl2an 456	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> (x e. (A(,)B) <-> (x e. RR /\ A < x /\ x < B)))
10	9	3adant3 801	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (x e. (A(,)B) <-> (x e. RR /\ A < x /\ x < B)))
11		3anass 781	. . . . . . . . . 10 |- ((x e. RR /\ A < x /\ x < B) <-> (x e. RR /\ (A < x /\ x < B)))
12	10, 11	syl6bb 538	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (x e. (A(,)B) <-> (x e. RR /\ (A < x /\ x < B))))
13		elico2t 6392	. . . . . . . . . . 11 |- ((B e. RR /\ C e. RR) -> (x e. (B[,)C) <-> (x e. RR /\ B <_ x /\ x < C)))
14	13	3adant1 799	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (x e. (B[,)C) <-> (x e. RR /\ B <_ x /\ x < C)))
15		3anass 781	. . . . . . . . . 10 |- ((x e. RR /\ B <_ x /\ x < C) <-> (x e. RR /\ (B <_ x /\ x < C)))
16	14, 15	syl6bb 538	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (x e. (B[,)C) <-> (x e. RR /\ (B <_ x /\ x < C))))
17	12, 16	orbi12d 629	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((x e. (A(,)B) \/ x e. (B[,)C)) <-> ((x e. RR /\ (A < x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C)))))
18	17	adantr 391	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) -> ((x e. (A(,)B) \/ x e. (B[,)C)) <-> ((x e. RR /\ (A < x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C)))))
19		pm2.24 79	. . . . . . . . . . . . . . . . 17 |- (A < x -> (-. A < x -> B <_ x))
20	19	ad2antrl 408	. . . . . . . . . . . . . . . 16 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> (-. A < x -> B <_ x))
21		lenltt 5522	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. RR /\ x e. RR) -> (B <_ x <-> -. x < B))
22	21	biimprd 154	. . . . . . . . . . . . . . . . . . 19 |- ((B e. RR /\ x e. RR) -> (-. x < B -> B <_ x))
23	22	3ad2antl2 812	. . . . . . . . . . . . . . . . . 18 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ x e. RR) -> (-. x < B -> B <_ x))
24	23	adantlr 395	. . . . . . . . . . . . . . . . 17 |- ((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) -> (-. x < B -> B <_ x))
25	24	adantr 391	. . . . . . . . . . . . . . . 16 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> (-. x < B -> B <_ x))
26	20, 25	jaod 426	. . . . . . . . . . . . . . 15 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> ((-. A < x \/ -. x < B) -> B <_ x))
27		ianor 305	. . . . . . . . . . . . . . 15 |- (-. (A < x /\ x < B) <-> (-. A < x \/ -. x < B))
28	26, 27	syl5ib 206	. . . . . . . . . . . . . 14 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> (-. (A < x /\ x < B) -> B <_ x))
29		pm3.27 323	. . . . . . . . . . . . . . . 16 |- ((A < x /\ x < C) -> x < C)
30	29	a1d 12	. . . . . . . . . . . . . . 15 |- ((A < x /\ x < C) -> (-. (A < x /\ x < B) -> x < C))
31	30	adantl 390	. . . . . . . . . . . . . 14 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> (-. (A < x /\ x < B) -> x < C))
32	28, 31	jcad 602	. . . . . . . . . . . . 13 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> (-. (A < x /\ x < B) -> (B <_ x /\ x < C)))
33	32	orrd 233	. . . . . . . . . . . 12 |- (((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) /\ (A < x /\ x < C)) -> ((A < x /\ x < B) \/ (B <_ x /\ x < C)))
34	33	ex 373	. . . . . . . . . . 11 |- ((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) -> ((A < x /\ x < C) -> ((A < x /\ x < B) \/ (B <_ x /\ x < C))))
35		axlttrn 5516	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. RR /\ B e. RR /\ C e. RR) -> ((x < B /\ B < C) -> x < C))
36	35	exp3a 376	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. RR /\ B e. RR /\ C e. RR) -> (x < B -> (B < C -> x < C)))
37	36	com23 32	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ B e. RR /\ C e. RR) -> (B < C -> (x < B -> x < C)))
38	37	3exp 834	. . . . . . . . . . . . . . . . . 18 |- (x e. RR -> (B e. RR -> (C e. RR -> (B < C -> (x < B -> x < C)))))
39	38	com4l 39	. . . . . . . . . . . . . . . . 17 |- (B e. RR -> (C e. RR -> (B < C -> (x e. RR -> (x < B -> x < C)))))
40	39	imp31 362	. . . . . . . . . . . . . . . 16 |- (((B e. RR /\ C e. RR) /\ B < C) -> (x e. RR -> (x < B -> x < C)))
41	40	3adantl1 805	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ B < C) -> (x e. RR -> (x < B -> x < C)))
42	41	adantrl 396	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) -> (x e. RR -> (x < B -> x < C)))
43	42	imp 350	. . . . . . . . . . . . 13 |- ((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) -> (x < B -> x < C))
44	43	anim2d 563	. . . . . . . . . . . 12 |- ((((A e. RR /\ B e. RR /\ C e. RR) /\ (A < B /\ B < C)) /\ x e. RR) -> ((A < x /\ x < B) -> (A < x /\ x < C)))
45		ltletrt 5536	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. RR /\ B e. RR /\ x e. RR) -> ((A < B /\ B <_ x) -> A < x))
46	45	exp3a 376	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ B e. RR /\ x e. RR) -> (A < B -> (B <_ x -> A < x)))
47	46	3exp 834	. . . . . . . . . . . . . . . . . 18 |- (A e. RR -> (B e. RR -> (x e. RR -> (A < B -> (B <_ x -> A < x)))))
48	47	com34 36	. . . . . . . . . . . . . . . . 17 |- (A e. RR -> (B e. RR -> (A < B -> (x e. RR -> (B <_ x -> A < x)))))
49	48	imp31 362	. . . . . . . . . . . . . . . 16 |- (((A e. RR /\ B e. RR) /\ A < B) -> (x e. RR -> (B <_ x -> A < x)))
50	49	3adantl3 807	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR /\ C e. RR