ixxss12

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ixx.1	$⊢ O = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x R z \land z S y)\})$
2		ixxss12.2	$⊢ P = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x T z \land z U y)\})$
3		ixxss12.3	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land w \in ℝ^{*}) \to ((A W C \land C T w) \to A R w)$
4		ixxss12.4	$⊢ (w \in ℝ^{} \land D \in ℝ^{} \land B \in ℝ^{*}) \to ((w U D \land D X B) \to w S B)$
5	2	elixx3g	$⊢ w \in (C P D) \leftrightarrow ((C \in ℝ^{} \land D \in ℝ^{} \land w \in ℝ^{*}) \land (C T w \land w U D))$
6	5	simplbi	$⊢ w \in (C P D) \to (C \in ℝ^{} \land D \in ℝ^{} \land w \in ℝ^{*})$
7	6	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to (C \in ℝ^{} \land D \in ℝ^{} \land w \in ℝ^{*})$
8	7	simp3d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to w \in ℝ^{*}$
9		simplrl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to A W C$
10	5	simprbi	$⊢ w \in (C P D) \to (C T w \land w U D)$
11	10	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to (C T w \land w U D)$
12	11	simpld	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to C T w$
13		simplll	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to A \in ℝ^{*}$
14	7	simp1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to C \in ℝ^{*}$
15	13 14 8 3	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to ((A W C \land C T w) \to A R w)$
16	9 12 15	mp2and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to A R w$
17	11	simprd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to w U D$
18		simplrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to D X B$
19	7	simp2d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to D \in ℝ^{*}$
20		simpllr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to B \in ℝ^{*}$
21	8 19 20 4	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to ((w U D \land D X B) \to w S B)$
22	17 18 21	mp2and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to w S B$
23	1	elixx1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{*} \land A R w \land w S B))$
24	23	ad2antrr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to (w \in (A O B) \leftrightarrow (w \in ℝ^{*} \land A R w \land w S B))$
25	8 16 22 24	mpbir3and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \land w \in (C P D)) \to w \in (A O B)$
26	25	ex	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \to (w \in (C P D) \to w \in (A O B))$
27	26	ssrdv	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A W C \land D X B)) \to C P D \subseteq A O B$

Metamath Proof Explorer

Theorem ixxss12

Proof