suplesup2

Description: If any element of A is less than or equal to an element in B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	suplesup2.a	$⊢ φ \to A \subseteq ℝ^{*}$
	suplesup2.b	$⊢ φ \to B \subseteq ℝ^{*}$
	suplesup2.c	$⊢ (φ \land x \in A) \to \exists y \in B x \leq y$
Assertion	suplesup2	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		suplesup2.a	$⊢ φ \to A \subseteq ℝ^{*}$
2		suplesup2.b	$⊢ φ \to B \subseteq ℝ^{*}$
3		suplesup2.c	$⊢ (φ \land x \in A) \to \exists y \in B x \leq y$
4	1	sselda	$⊢ (φ \land x \in A) \to x \in ℝ^{*}$
5	4	3ad2ant1	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to x \in ℝ^{*}$
6		simp1l	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to φ$
7		simp2	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to y \in B$
8	2	sselda	$⊢ (φ \land y \in B) \to y \in ℝ^{*}$
9	6 7 8	syl2anc	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to y \in ℝ^{*}$
10		supxrcl	$⊢ B \subseteq ℝ^{} \to sup (B ℝ^{} <) \in ℝ^{*}$
11	2 10	syl	$⊢ φ \to sup (B ℝ^{} <) \in ℝ^{}$
12	6 11	syl	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to sup (B ℝ^{} <) \in ℝ^{}$
13		simp3	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to x \leq y$
14	2	adantr	$⊢ (φ \land y \in B) \to B \subseteq ℝ^{*}$
15		simpr	$⊢ (φ \land y \in B) \to y \in B$
16		supxrub	$⊢ (B \subseteq ℝ^{} \land y \in B) \to y \leq sup (B ℝ^{} <)$
17	14 15 16	syl2anc	$⊢ (φ \land y \in B) \to y \leq sup (B ℝ^{*} <)$
18	6 7 17	syl2anc	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to y \leq sup (B ℝ^{*} <)$
19	5 9 12 13 18	xrletrd	$⊢ ((φ \land x \in A) \land y \in B \land x \leq y) \to x \leq sup (B ℝ^{*} <)$
20	19	3exp	$⊢ (φ \land x \in A) \to (y \in B \to (x \leq y \to x \leq sup (B ℝ^{*} <)))$
21	20	rexlimdv	$⊢ (φ \land x \in A) \to (\exists y \in B x \leq y \to x \leq sup (B ℝ^{*} <))$
22	3 21	mpd	$⊢ (φ \land x \in A) \to x \leq sup (B ℝ^{*} <)$
23	22	ralrimiva	$⊢ φ \to \forall x \in A x \leq sup (B ℝ^{*} <)$
24		supxrleub	$⊢ (A \subseteq ℝ^{} \land sup (B ℝ^{} <) \in ℝ^{}) \to (sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (B ℝ^{} <))$
25	1 11 24	syl2anc	$⊢ φ \to (sup (A ℝ^{} <) \leq sup (B ℝ^{} <) \leftrightarrow \forall x \in A x \leq sup (B ℝ^{*} <))$
26	23 25	mpbird	$⊢ φ \to sup (A ℝ^{} <) \leq sup (B ℝ^{} <)$

Metamath Proof Explorer

Theorem suplesup2

Proof