ixxun

Description: Split an interval into two parts. (Contributed by Mario Carneiro, 16-Jun-2014)

	Ref	Expression
Hypotheses	ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
	ixxun.2	$⊢ P = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x T z \land z U y)\})$
	ixxun.3	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B T w \leftrightarrow \neg w S B)$
	ixxun.4	$⊢ Q = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z U y)\})$
	ixxun.5	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w S B \land B X C) \to w U C)$
	ixxun.6	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A W B \land B T w) \to A R w)$
Assertion	ixxun	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \to (A O B) \cup (B P C) = A Q C$

Proof

Step	Hyp	Ref	Expression
1		ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
2		ixxun.2	$⊢ P = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x T z \land z U y)\})$
3		ixxun.3	$⊢ (B \in ℝ^{} \land w \in ℝ^{}) \to (B T w \leftrightarrow \neg w S B)$
4		ixxun.4	$⊢ Q = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z U y)\})$
5		ixxun.5	$⊢ (w \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to ((w S B \land B X C) \to w U C)$
6		ixxun.6	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A W B \land B T w) \to A R w)$
7		elun	$⊢ w \in ((A O B) \cup (B P C)) \leftrightarrow (w \in (A O B) \lor w \in (B P C))$
8		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to A \in ℝ^{}$
9		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to B \in ℝ^{}$
10	1	elixx1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{*} \land A R w \land w S B))$
11	8 9 10	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{} \land A R w \land w S B))$
12	11	biimpa	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A O B)) \to (w \in ℝ^{} \land A R w \land w S B)$
13	12	simp1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A O B)) \to w \in ℝ^{}$
14	12	simp2d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A O B)) \to A R w$
15	12	simp3d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A O B)) \to w S B$
16		simplrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A O B)) \to B X C$
17	9	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A O B)) \to B \in ℝ^{}$
18		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to C \in ℝ^{}$
19	18	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A O B)) \to C \in ℝ^{}$
20	13 17 19 5	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A O B)) \to ((w S B \land B X C) \to w U C)$
21	15 16 20	mp2and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A O B)) \to w U C$
22	13 14 21	3jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A O B)) \to (w \in ℝ^{} \land A R w \land w U C)$
23	2	elixx1	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to (w \in (B P C) \leftrightarrow (w \in ℝ^{*} \land B T w \land w U C))$
24	9 18 23	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to (w \in (B P C) \leftrightarrow (w \in ℝ^{} \land B T w \land w U C))$
25	24	biimpa	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (B P C)) \to (w \in ℝ^{} \land B T w \land w U C)$
26	25	simp1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (B P C)) \to w \in ℝ^{}$
27		simplrl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (B P C)) \to A W B$
28	25	simp2d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (B P C)) \to B T w$
29	8	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (B P C)) \to A \in ℝ^{}$
30	9	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (B P C)) \to B \in ℝ^{}$
31	29 30 26 6	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (B P C)) \to ((A W B \land B T w) \to A R w)$
32	27 28 31	mp2and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (B P C)) \to A R w$
33	25	simp3d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (B P C)) \to w U C$
34	26 32 33	3jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (B P C)) \to (w \in ℝ^{} \land A R w \land w U C)$
35	22 34	jaodan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land (w \in (A O B) \lor w \in (B P C))) \to (w \in ℝ^{} \land A R w \land w U C)$
36	4	elixx1	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to (w \in (A Q C) \leftrightarrow (w \in ℝ^{*} \land A R w \land w U C))$
37	8 18 36	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to (w \in (A Q C) \leftrightarrow (w \in ℝ^{} \land A R w \land w U C))$
38	37	biimpar	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land (w \in ℝ^{} \land A R w \land w U C)) \to w \in (A Q C)$
39	35 38	syldan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land (w \in (A O B) \lor w \in (B P C))) \to w \in (A Q C)$
40		exmid	$⊢ (w S B \lor \neg w S B)$
41	37	biimpa	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in ℝ^{} \land A R w \land w U C)$
42	41	simp1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to w \in ℝ^{}$
43	41	simp2d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to A R w$
44	42 43	jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in ℝ^{} \land A R w)$
45		df-3an	$⊢ (w \in ℝ^{} \land A R w \land w S B) \leftrightarrow ((w \in ℝ^{} \land A R w) \land w S B)$
46	11 45	bitrdi	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to (w \in (A O B) \leftrightarrow ((w \in ℝ^{} \land A R w) \land w S B))$
47	46	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in (A O B) \leftrightarrow ((w \in ℝ^{} \land A R w) \land w S B))$
48	44 47	mpbirand	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in (A O B) \leftrightarrow w S B)$
49		3anan12	$⊢ (w \in ℝ^{} \land B T w \land w U C) \leftrightarrow (B T w \land (w \in ℝ^{} \land w U C))$
50	24 49	bitrdi	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \to (w \in (B P C) \leftrightarrow (B T w \land (w \in ℝ^{} \land w U C)))$
51	50	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in (B P C) \leftrightarrow (B T w \land (w \in ℝ^{} \land w U C)))$
52	41	simp3d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to w U C$
53	42 52	jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in ℝ^{} \land w U C)$
54	53	biantrud	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (B T w \leftrightarrow (B T w \land (w \in ℝ^{} \land w U C)))$
55	9	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land (A W B \land B X C)) \land w \in (A Q C)) \to B \in ℝ^{}$
56	55 42 3	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (B T w \leftrightarrow \neg w S B)$
57	51 54 56	3bitr2d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in (B P C) \leftrightarrow \neg w S B)$
58	48 57	orbi12d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to ((w \in (A O B) \lor w \in (B P C)) \leftrightarrow (w S B \lor \neg w S B))$
59	40 58	mpbiri	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \land w \in (A Q C)) \to (w \in (A O B) \lor w \in (B P C))$
60	39 59	impbida	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \to ((w \in (A O B) \lor w \in (B P C)) \leftrightarrow w \in (A Q C))$
61	7 60	bitrid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \to (w \in ((A O B) \cup (B P C)) \leftrightarrow w \in (A Q C))$
62	61	eqrdv	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A W B \land B X C)) \to (A O B) \cup (B P C) = A Q C$

Metamath Proof Explorer

Theorem ixxun

Proof