ixxss1

Description: Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013) (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)\})$
	ixxss1.2	$⊢ P = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x T z \land z S y)\})$
	ixxss1.3	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land w \in ℝ^{*}) \to ((A W B \land B T w) \to A R w)$
Assertion	ixxss1	$⊢ (A \in ℝ^{*} \land A W B) \to B P C \subseteq A O C$

Proof

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

Metamath Proof Explorer

Theorem ixxss1

Proof