Theorem icounlem 6412

Description: Lemma for icoun 6413.

Hypotheses

Ref	Expression
icounlem.1	|- A e. RR
icounlem.2	|- B e. RR
icounlem.3	|- C e. RR

Assertion

Ref	Expression
icounlem	|- ((A <_ B /\ B <_ C) -> ((A[,)B) u. (B[,)C)) = (A[,)C))

Proof of Theorem icounlem

Step	Hyp	Ref	Expression
1		icounlem.1	. . . . . . . . . . . . . . . . 17 |- A e. RR
2		icounlem.2	. . . . . . . . . . . . . . . . 17 |- B e. RR
3		letrt 5525	. . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ B e. RR /\ x e. RR) -> ((A <_ B /\ B <_ x) -> A <_ x))
4	1, 2, 3	mp3an12 906	. . . . . . . . . . . . . . . 16 |- (x e. RR -> ((A <_ B /\ B <_ x) -> A <_ x))
5	4	exp3a 375	. . . . . . . . . . . . . . 15 |- (x e. RR -> (A <_ B -> (B <_ x -> A <_ x)))
6	5	imp 350	. . . . . . . . . . . . . 14 |- ((x e. RR /\ A <_ B) -> (B <_ x -> A <_ x))
7		pm4.72 641	. . . . . . . . . . . . . 14 |- ((B <_ x -> A <_ x) <-> (A <_ x <-> (B <_ x \/ A <_ x)))
8	6, 7	sylib 198	. . . . . . . . . . . . 13 |- ((x e. RR /\ A <_ B) -> (A <_ x <-> (B <_ x \/ A <_ x)))
9	8	adantrr 395	. . . . . . . . . . . 12 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> (B <_ x \/ A <_ x)))
10		orcom 246	. . . . . . . . . . . 12 |- ((B <_ x \/ A <_ x) <-> (A <_ x \/ B <_ x))
11	9, 10	syl6bb 536	. . . . . . . . . . 11 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> (A <_ x \/ B <_ x)))
12		ltnlet 5511	. . . . . . . . . . . . . . . . 17 |- ((x e. RR /\ A e. RR) -> (x < A <-> -. A <_ x))
13	1, 12	mpan2 696	. . . . . . . . . . . . . . . 16 |- (x e. RR -> (x < A <-> -. A <_ x))
14	13	adantr 389	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ A <_ C) -> (x < A <-> -. A <_ x))
15		icounlem.3	. . . . . . . . . . . . . . . . . . 19 |- C e. RR
16		ltletrt 5524	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ A e. RR /\ C e. RR) -> ((x < A /\ A <_ C) -> x < C))
17	1, 15, 16	mp3an23 908	. . . . . . . . . . . . . . . . . 18 |- (x e. RR -> ((x < A /\ A <_ C) -> x < C))
18	17	exp3a 375	. . . . . . . . . . . . . . . . 17 |- (x e. RR -> (x < A -> (A <_ C -> x < C)))
19	18	com23 32	. . . . . . . . . . . . . . . 16 |- (x e. RR -> (A <_ C -> (x < A -> x < C)))
20	19	imp 350	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ A <_ C) -> (x < A -> x < C))
21	14, 20	sylbird 205	. . . . . . . . . . . . . 14 |- ((x e. RR /\ A <_ C) -> (-. A <_ x -> x < C))
22	21	orrd 233	. . . . . . . . . . . . 13 |- ((x e. RR /\ A <_ C) -> (A <_ x \/ x < C))
23	1, 2, 15	letr 5588	. . . . . . . . . . . . 13 |- ((A <_ B /\ B <_ C) -> A <_ C)
24	22, 23	sylan2 451	. . . . . . . . . . . 12 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x \/ x < C))
25	24	biantrurd 727	. . . . . . . . . . 11 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((A <_ x \/ B <_ x) <-> ((A <_ x \/ x < C) /\ (A <_ x \/ B <_ x))))
26	11, 25	bitrd 528	. . . . . . . . . 10 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> ((A <_ x \/ x < C) /\ (A <_ x \/ B <_ x))))
27		ancom 435	. . . . . . . . . 10 |- (((A <_ x \/ x < C) /\ (A <_ x \/ B <_ x)) <-> ((A <_ x \/ B <_ x) /\ (A <_ x \/ x < C)))
28	26, 27	syl6bb 536	. . . . . . . . 9 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> ((A <_ x \/ B <_ x) /\ (A <_ x \/ x < C))))
29		ltletrt 5524	. . . . . . . . . . . . . . . 16 |- ((x e. RR /\ B e. RR /\ C e. RR) -> ((x < B /\ B <_ C) -> x < C))
30	2, 15, 29	mp3an23 908	. . . . . . . . . . . . . . 15 |- (x e. RR -> ((x < B /\ B <_ C) -> x < C))
31	30	exp3a 375	. . . . . . . . . . . . . 14 |- (x e. RR -> (x < B -> (B <_ C -> x < C)))
32	31	com23 32	. . . . . . . . . . . . 13 |- (x e. RR -> (B <_ C -> (x < B -> x < C)))
33	32	imp 350	. . . . . . . . . . . 12 |- ((x e. RR /\ B <_ C) -> (x < B -> x < C))
34		pm4.72 641	. . . . . . . . . . . 12 |- ((x < B -> x < C) <-> (x < C <-> (x < B \/ x < C)))
35	33, 34	sylib 198	. . . . . . . . . . 11 |- ((x e. RR /\ B <_ C) -> (x < C <-> (x < B \/ x < C)))
36	35	adantrl 394	. . . . . . . . . 10 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (x < C <-> (x < B \/ x < C)))
37		lelttrit 5622	. . . . . . . . . . . . . 14 |- ((B e. RR /\ x e. RR) -> (B <_ x \/ x < B))
38	2, 37	mpan 695	. . . . . . . . . . . . 13 |- (x e. RR -> (B <_ x \/ x < B))
39		orcom 246	. . . . . . . . . . . . 13 |- ((B <_ x \/ x < B) <-> (x < B \/ B <_ x))
40	38, 39	sylib 198	. . . . . . . . . . . 12 |- (x e. RR -> (x < B \/ B <_ x))
41	40	adantr 389	. . . . . . . . . . 11 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (x < B \/ B <_ x))
42	41	biantrurd 727	. . . . . . . . . 10 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((x < B \/ x < C) <-> ((x < B \/ B <_ x) /\ (x < B \/ x < C))))
43	36, 42	bitrd 528	. . . . . . . . 9 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (x < C <-> ((x < B \/ B <_ x) /\ (x < B \/ x < C))))
44	28, 43	anbi12d 628	. . . . . . . 8 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((A <_ x /\ x < C) <-> (((A <_ x \/ B <_ x) /\ (A <_ x \/ x < C)) /\ ((x < B \/ B <_ x) /\ (x < B \/ x < C)))))
45		orddi 606	. . . . . . . 8 |- (((A <_ x /\ x < B) \/ (B <_ x /\ x < C)) <-> (((A <_ x \/ B <_ x) /\ (A <_ x \/ x < C)) /\ ((x < B \/ B <_ x) /\ (x < B \/ x < C))))
46	44, 45	syl6bbr 538	. . . . . . 7 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((A <_ x /\ x < C) <-> ((A <_ x /\ x < B) \/ (B <_ x /\ x < C))))
47	46	expcom 374	. . . . . 6 |- ((A <_ B /\ B <_ C) -> (x e. RR -> ((A <_ x /\ x < C) <-> ((A <_ x /\ x < B) \/ (B <_ x /\ x < C)))))
48	47	pm5.32d 647	. . . . 5 |- ((A <_ B /\ B <_ C) -> ((x e. RR /\ (A <_ x /\ x < C)) <-> (x e. RR /\ ((A <_ x /\ x < B) \/ (B <_ x /\ x < C)))))
49		andi 604	. . . . 5 |- ((x e. RR /\ ((A <_ x /\ x < B) \/ (B <_ x /\ x < C))) <-> ((x e. RR /\ (A <_ x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C))))
50	48, 49	syl6bb 536	. . . 4 |- ((A <_ B /\ B <_ C) -> ((x e. RR /\ (A <_ x /\ x < C)) <-> ((x e. RR /\ (A <_ x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C)))))
51		elico2t 6391	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (x e. (A[,)B) <-> (x e. RR /\ A <_ x /\ x < B)))
52	1, 2, 51	mp2an 697	. . . . . 6 |- (x e. (A[,)B) <-> (x e. RR /\ A <_ x /\ x < B))
53		elico2t 6391	. . . . . . 7 |- ((B e. RR /\ C e. RR) -> (x e. (B[,)C) <-> (x e. RR /\ B <_ x /\ x < C)))
54	2, 15, 53	mp2an 697	. . . . . 6 |- (x e. (B[,)C) <-> (x e. RR /\ B <_ x /\ x < C))
55	52, 54	orbi12i 257	. . . . 5 |- ((x e. (A[,)B) \/ x e. (B[,)C)) <-> ((x e. RR /\ A <_ x /\ x < B) \/ (x e. RR /\ B <_ x /\ x < C)))
56		3anass 779	. . . . . 6 |- ((x e. RR /\ A <_ x /\ x < B) <-> (x e. RR /\ (A <_ x /\ x < B)))
57		3anass 779	. . . . . 6 |- ((x e. RR /\ B <_ x /\ x < C) <-> (x e. RR /\ (B <_ x /\ x < C)))
58	56, 57	orbi12i 257	. . . . 5 |- (((x e. RR /\ A <_ x /\ x < B) \/ (x e. RR /\ B <_ x /\ x < C)) <-> ((x e. RR /\ (A <_ x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C))))
59	55, 58	bitr 173	. . . 4 |- ((x e. (A[,)B) \/ x e. (B[,)C)) <-> ((x e. RR /\ (A <_ x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C))))
60	50, 59	syl6rbbr 539	. . 3 |- ((A <_ B /\ B <_ C) -> ((x e. (A[,)B) \/ x e. (B[,)C)) <-> (x e. RR /\ (A