ioossioobi

	Ref	Expression
Hypotheses	ioossioobi.a	$⊢ φ \to A \in ℝ^{*}$
	ioossioobi.b	$⊢ φ \to B \in ℝ^{*}$
	ioossioobi.c	$⊢ φ \to C \in ℝ^{*}$
	ioossioobi.d	$⊢ φ \to D \in ℝ^{*}$
	ioossioobi.cltd	$⊢ φ \to C < D$
Assertion	ioossioobi	$⊢ φ \to ((C, D) \subseteq (A, B) \leftrightarrow (A \leq C \land D \leq B))$

Proof

Step	Hyp	Ref	Expression
1		ioossioobi.a	$⊢ φ \to A \in ℝ^{*}$
2		ioossioobi.b	$⊢ φ \to B \in ℝ^{*}$
3		ioossioobi.c	$⊢ φ \to C \in ℝ^{*}$
4		ioossioobi.d	$⊢ φ \to D \in ℝ^{*}$
5		ioossioobi.cltd	$⊢ φ \to C < D$
6		simpr	$⊢ (φ \land (C, D) \subseteq (A, B)) \to (C, D) \subseteq (A, B)$
7		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
8	7	ixxssxr	$⊢ (A, B) \subseteq ℝ^{*}$
9		infxrss	$⊢ ((C, D) \subseteq (A, B) \land (A, B) \subseteq ℝ^{}) \to inf ((A, B) ℝ^{} <) \leq inf ((C, D) ℝ^{*} <)$
10	6 8 9	sylancl	$⊢ (φ \land (C, D) \subseteq (A, B)) \to inf ((A, B) ℝ^{} <) \leq inf ((C, D) ℝ^{} <)$
11	1	adantr	$⊢ (φ \land (C, D) \subseteq (A, B)) \to A \in ℝ^{*}$
12	2	adantr	$⊢ (φ \land (C, D) \subseteq (A, B)) \to B \in ℝ^{*}$
13		ioon0	$⊢ (C \in ℝ^{} \land D \in ℝ^{}) \to ((C, D) \neq \emptyset \leftrightarrow C < D)$
14	3 4 13	syl2anc	$⊢ φ \to ((C, D) \neq \emptyset \leftrightarrow C < D)$
15	5 14	mpbird	$⊢ φ \to (C, D) \neq \emptyset$
16	15	adantr	$⊢ (φ \land (C, D) \subseteq (A, B)) \to (C, D) \neq \emptyset$
17		ssn0	$⊢ ((C, D) \subseteq (A, B) \land (C, D) \neq \emptyset) \to (A, B) \neq \emptyset$
18	6 16 17	syl2anc	$⊢ (φ \land (C, D) \subseteq (A, B)) \to (A, B) \neq \emptyset$
19		idd	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w < B \to w < B)$
20		xrltle	$⊢ (w \in ℝ^{} \land B \in ℝ^{}) \to (w < B \to w \leq B)$
21		idd	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A < w)$
22		xrltle	$⊢ (A \in ℝ^{} \land w \in ℝ^{}) \to (A < w \to A \leq w)$
23	7 19 20 21 22	ixxlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land (A, B) \neq \emptyset) \to inf ((A, B) ℝ^{*} <) = A$
24	11 12 18 23	syl3anc	$⊢ (φ \land (C, D) \subseteq (A, B)) \to inf ((A, B) ℝ^{*} <) = A$
25	3	adantr	$⊢ (φ \land (C, D) \subseteq (A, B)) \to C \in ℝ^{*}$
26	4	adantr	$⊢ (φ \land (C, D) \subseteq (A, B)) \to D \in ℝ^{*}$
27		idd	$⊢ (w \in ℝ^{} \land D \in ℝ^{}) \to (w < D \to w < D)$
28		xrltle	$⊢ (w \in ℝ^{} \land D \in ℝ^{}) \to (w < D \to w \leq D)$
29		idd	$⊢ (C \in ℝ^{} \land w \in ℝ^{}) \to (C < w \to C < w)$
30		xrltle	$⊢ (C \in ℝ^{} \land w \in ℝ^{}) \to (C < w \to C \leq w)$
31	7 27 28 29 30	ixxlb	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land (C, D) \neq \emptyset) \to inf ((C, D) ℝ^{*} <) = C$
32	25 26 16 31	syl3anc	$⊢ (φ \land (C, D) \subseteq (A, B)) \to inf ((C, D) ℝ^{*} <) = C$
33	10 24 32	3brtr3d	$⊢ (φ \land (C, D) \subseteq (A, B)) \to A \leq C$
34		supxrss	$⊢ ((C, D) \subseteq (A, B) \land (A, B) \subseteq ℝ^{}) \to sup ((C, D) ℝ^{} <) \leq sup ((A, B) ℝ^{*} <)$
35	6 8 34	sylancl	$⊢ (φ \land (C, D) \subseteq (A, B)) \to sup ((C, D) ℝ^{} <) \leq sup ((A, B) ℝ^{} <)$
36	7 27 28 29 30	ixxub	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land (C, D) \neq \emptyset) \to sup ((C, D) ℝ^{*} <) = D$
37	25 26 16 36	syl3anc	$⊢ (φ \land (C, D) \subseteq (A, B)) \to sup ((C, D) ℝ^{*} <) = D$
38	7 19 20 21 22	ixxub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land (A, B) \neq \emptyset) \to sup ((A, B) ℝ^{*} <) = B$
39	11 12 18 38	syl3anc	$⊢ (φ \land (C, D) \subseteq (A, B)) \to sup ((A, B) ℝ^{*} <) = B$
40	35 37 39	3brtr3d	$⊢ (φ \land (C, D) \subseteq (A, B)) \to D \leq B$
41	33 40	jca	$⊢ (φ \land (C, D) \subseteq (A, B)) \to (A \leq C \land D \leq B)$
42	1	adantr	$⊢ (φ \land (A \leq C \land D \leq B)) \to A \in ℝ^{*}$
43	2	adantr	$⊢ (φ \land (A \leq C \land D \leq B)) \to B \in ℝ^{*}$
44		simprl	$⊢ (φ \land (A \leq C \land D \leq B)) \to A \leq C$
45		simprr	$⊢ (φ \land (A \leq C \land D \leq B)) \to D \leq B$
46		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq C \land D \leq B)) \to (C, D) \subseteq (A, B)$
47	42 43 44 45 46	syl22anc	$⊢ (φ \land (A \leq C \land D \leq B)) \to (C, D) \subseteq (A, B)$
48	41 47	impbida	$⊢ φ \to ((C, D) \subseteq (A, B) \leftrightarrow (A \leq C \land D \leq B))$

Metamath Proof Explorer

Theorem ioossioobi

Proof