Theorem icounlem 6472

Description: Lemma for icoun 6473.

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	. . . . . . . . . . . . . . . 16 |- A e. RR
2		icounlem.2	. . . . . . . . . . . . . . . 16 |- B e. RR
3		letr 5614	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ B e. RR /\ x e. RR) -> ((A <_ B /\ B <_ x) -> A <_ x))
4	1, 2, 3	mp3an12 909	. . . . . . . . . . . . . . 15 |- (x e. RR -> ((A <_ B /\ B <_ x) -> A <_ x))
5	4	expdimp 375	. . . . . . . . . . . . . 14 |- ((x e. RR /\ A <_ B) -> (B <_ x -> A <_ x))
6		pm4.72 643	. . . . . . . . . . . . . 14 |- ((B <_ x -> A <_ x) <-> (A <_ x <-> (B <_ x \/ A <_ x)))
7	5, 6	sylib 196	. . . . . . . . . . . . 13 |- ((x e. RR /\ A <_ B) -> (A <_ x <-> (B <_ x \/ A <_ x)))
8	7	adantrr 395	. . . . . . . . . . . 12 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> (B <_ x \/ A <_ x)))
9		orcom 244	. . . . . . . . . . . 12 |- ((B <_ x \/ A <_ x) <-> (A <_ x \/ B <_ x))
10	8, 9	syl6bb 538	. . . . . . . . . . 11 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> (A <_ x \/ B <_ x)))
11		ltnle 5600	. . . . . . . . . . . . . . . . 17 |- ((x e. RR /\ A e. RR) -> (x < A <-> -. A <_ x))
12	1, 11	mpan2 699	. . . . . . . . . . . . . . . 16 |- (x e. RR -> (x < A <-> -. A <_ x))
13	12	adantr 389	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ A <_ C) -> (x < A <-> -. A <_ x))
14		icounlem.3	. . . . . . . . . . . . . . . . . . 19 |- C e. RR
15		ltletr 5613	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ A e. RR /\ C e. RR) -> ((x < A /\ A <_ C) -> x < C))
16	1, 14, 15	mp3an23 911	. . . . . . . . . . . . . . . . . 18 |- (x e. RR -> ((x < A /\ A <_ C) -> x < C))
17	16	exp3a 374	. . . . . . . . . . . . . . . . 17 |- (x e. RR -> (x < A -> (A <_ C -> x < C)))
18	17	com23 32	. . . . . . . . . . . . . . . 16 |- (x e. RR -> (A <_ C -> (x < A -> x < C)))
19	18	imp 348	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ A <_ C) -> (x < A -> x < C))
20	13, 19	sylbird 203	. . . . . . . . . . . . . 14 |- ((x e. RR /\ A <_ C) -> (-. A <_ x -> x < C))
21	20	orrd 231	. . . . . . . . . . . . 13 |- ((x e. RR /\ A <_ C) -> (A <_ x \/ x < C))
22	1, 2, 14	letri 5677	. . . . . . . . . . . . 13 |- ((A <_ B /\ B <_ C) -> A <_ C)
23	21, 22	sylan2 453	. . . . . . . . . . . 12 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x \/ x < C))
24	23	biantrurd 730	. . . . . . . . . . 11 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((A <_ x \/ B <_ x) <-> ((A <_ x \/ x < C) /\ (A <_ x \/ B <_ x))))
25	10, 24	bitrd 530	. . . . . . . . . 10 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> ((A <_ x \/ x < C) /\ (A <_ x \/ B <_ x))))
26		ancom 437	. . . . . . . . . 10 |- (((A <_ x \/ x < C) /\ (A <_ x \/ B <_ x)) <-> ((A <_ x \/ B <_ x) /\ (A <_ x \/ x < C)))
27	25, 26	syl6bb 538	. . . . . . . . 9 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (A <_ x <-> ((A <_ x \/ B <_ x) /\ (A <_ x \/ x < C))))
28		ltletr 5613	. . . . . . . . . . . . . . . 16 |- ((x e. RR /\ B e. RR /\ C e. RR) -> ((x < B /\ B <_ C) -> x < C))
29	2, 14, 28	mp3an23 911	. . . . . . . . . . . . . . 15 |- (x e. RR -> ((x < B /\ B <_ C) -> x < C))
30	29	exp3a 374	. . . . . . . . . . . . . 14 |- (x e. RR -> (x < B -> (B <_ C -> x < C)))
31	30	com23 32	. . . . . . . . . . . . 13 |- (x e. RR -> (B <_ C -> (x < B -> x < C)))
32	31	imp 348	. . . . . . . . . . . 12 |- ((x e. RR /\ B <_ C) -> (x < B -> x < C))
33		pm4.72 643	. . . . . . . . . . . 12 |- ((x < B -> x < C) <-> (x < C <-> (x < B \/ x < C)))
34	32, 33	sylib 196	. . . . . . . . . . 11 |- ((x e. RR /\ B <_ C) -> (x < C <-> (x < B \/ x < C)))
35	34	adantrl 394	. . . . . . . . . 10 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (x < C <-> (x < B \/ x < C)))
36		lelttric 5711	. . . . . . . . . . . . . 14 |- ((B e. RR /\ x e. RR) -> (B <_ x \/ x < B))
37	2, 36	mpan 698	. . . . . . . . . . . . 13 |- (x e. RR -> (B <_ x \/ x < B))
38		orcom 244	. . . . . . . . . . . . 13 |- ((B <_ x \/ x < B) <-> (x < B \/ B <_ x))
39	37, 38	sylib 196	. . . . . . . . . . . 12 |- (x e. RR -> (x < B \/ B <_ x))
40	39	adantr 389	. . . . . . . . . . 11 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (x < B \/ B <_ x))
41	40	biantrurd 730	. . . . . . . . . 10 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((x < B \/ x < C) <-> ((x < B \/ B <_ x) /\ (x < B \/ x < C))))
42	35, 41	bitrd 530	. . . . . . . . 9 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> (x < C <-> ((x < B \/ B <_ x) /\ (x < B \/ x < C))))
43	27, 42	anbi12d 630	. . . . . . . 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)))))
44		orddi 608	. . . . . . . 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))))
45	43, 44	syl6bbr 540	. . . . . . 7 |- ((x e. RR /\ (A <_ B /\ B <_ C)) -> ((A <_ x /\ x < C) <-> ((A <_ x /\ x < B) \/ (B <_ x /\ x < C))))
46	45	expcom 372	. . . . . 6 |- ((A <_ B /\ B <_ C) -> (x e. RR -> ((A <_ x /\ x < C) <-> ((A <_ x /\ x < B) \/ (B <_ x /\ x < C)))))
47	46	pm5.32d 649	. . . . 5 |- ((A <_ B /\ B <_ C) -> ((x e. RR /\ (A <_ x /\ x < C)) <-> (x e. RR /\ ((A <_ x /\ x < B) \/ (B <_ x /\ x < C)))))
48		andi 606	. . . . 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))))
49	47, 48	syl6bb 538	. . . 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)))))
50		elico2 6450	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (x e. (A[,)B) <-> (x e. RR /\ A <_ x /\ x < B)))
51	1, 2, 50	mp2an 700	. . . . . 6 |- (x e. (A[,)B) <-> (x e. RR /\ A <_ x /\ x < B))
52		elico2 6450	. . . . . . 7 |- ((B e. RR /\ C e. RR) -> (x e. (B[,)C) <-> (x e. RR /\ B <_ x /\ x < C)))
53	2, 14, 52	mp2an 700	. . . . . 6 |- (x e. (B[,)C) <-> (x e. RR /\ B <_ x /\ x < C))
54	51, 53	orbi12i 255	. . . . 5 |- ((x e. (A[,)B) \/ x e. (B[,)C)) <-> ((x e. RR /\ A <_ x /\ x < B) \/ (x e. RR /\ B <_ x /\ x < C)))
55		3anass 782	. . . . . 6 |- ((x e. RR /\ A <_ x /\ x < B) <-> (x e. RR /\ (A <_ x /\ x < B)))
56		3anass 782	. . . . . 6 |- ((x e. RR /\ B <_ x /\ x < C) <-> (x e. RR /\ (B <_ x /\ x < C)))
57	55, 56	orbi12i 255	. . . . 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))))
58	54, 57	bitri 171	. . . 4 |- ((x e. (A[,)B) \/ x e. (B[,)C)) <-> ((x e. RR /\ (A <_ x /\ x < B)) \/ (x e. RR /\ (B <_ x /\ x < C))))
59	49, 58	syl6rbbr 541	. . 3 |- ((A <_ B /\ B <_ C) -> ((x e. (A[,)B) \/ x e. (B[,)C)) <-> (x e. RR /\ (A <_ x /\ x < C))))
60		elun 2217	. . 3 |- (x e. ((A[,)B) u. (B[,)