infleinf2

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

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

Proof

Step	Hyp	Ref	Expression
1		infleinf2.x	$⊢ Ⅎ x φ$
2		infleinf2.p	$⊢ Ⅎ y φ$
3		infleinf2.a	$⊢ φ \to A \subseteq ℝ^{*}$
4		infleinf2.b	$⊢ φ \to B \subseteq ℝ^{*}$
5		infleinf2.y	$⊢ (φ \land x \in B) \to \exists y \in A y \leq x$
6		nfv	$⊢ Ⅎ y x \in B$
7	2 6	nfan	$⊢ Ⅎ y (φ \land x \in B)$
8		nfv	$⊢ Ⅎ y inf (A ℝ^{*} <) \leq x$
9	3	infxrcld	$⊢ φ \to inf (A ℝ^{} <) \in ℝ^{}$
10	9	3ad2ant1	$⊢ (φ \land y \in A \land y \leq x) \to inf (A ℝ^{} <) \in ℝ^{}$
11	10	3adant1r	$⊢ ((φ \land x \in B) \land y \in A \land y \leq x) \to inf (A ℝ^{} <) \in ℝ^{}$
12	3	sselda	$⊢ (φ \land y \in A) \to y \in ℝ^{*}$
13	12	3adant3	$⊢ (φ \land y \in A \land y \leq x) \to y \in ℝ^{*}$
14	13	3adant1r	$⊢ ((φ \land x \in B) \land y \in A \land y \leq x) \to y \in ℝ^{*}$
15	4	sselda	$⊢ (φ \land x \in B) \to x \in ℝ^{*}$
16	15	3ad2ant1	$⊢ ((φ \land x \in B) \land y \in A \land y \leq x) \to x \in ℝ^{*}$
17	3	adantr	$⊢ (φ \land y \in A) \to A \subseteq ℝ^{*}$
18		simpr	$⊢ (φ \land y \in A) \to y \in A$
19		infxrlb	$⊢ (A \subseteq ℝ^{} \land y \in A) \to inf (A ℝ^{} <) \leq y$
20	17 18 19	syl2anc	$⊢ (φ \land y \in A) \to inf (A ℝ^{*} <) \leq y$
21	20	3adant3	$⊢ (φ \land y \in A \land y \leq x) \to inf (A ℝ^{*} <) \leq y$
22	21	3adant1r	$⊢ ((φ \land x \in B) \land y \in A \land y \leq x) \to inf (A ℝ^{*} <) \leq y$
23		simp3	$⊢ ((φ \land x \in B) \land y \in A \land y \leq x) \to y \leq x$
24	11 14 16 22 23	xrletrd	$⊢ ((φ \land x \in B) \land y \in A \land y \leq x) \to inf (A ℝ^{*} <) \leq x$
25	24	3exp	$⊢ (φ \land x \in B) \to (y \in A \to (y \leq x \to inf (A ℝ^{*} <) \leq x))$
26	7 8 25	rexlimd	$⊢ (φ \land x \in B) \to (\exists y \in A y \leq x \to inf (A ℝ^{*} <) \leq x)$
27	5 26	mpd	$⊢ (φ \land x \in B) \to inf (A ℝ^{*} <) \leq x$
28	1 27	ralrimia	$⊢ φ \to \forall x \in B inf (A ℝ^{*} <) \leq x$
29		infxrgelb	$⊢ (B \subseteq ℝ^{} \land inf (A ℝ^{} <) \in ℝ^{}) \to (inf (A ℝ^{} <) \leq inf (B ℝ^{} <) \leftrightarrow \forall x \in B inf (A ℝ^{} <) \leq x)$
30	4 9 29	syl2anc	$⊢ φ \to (inf (A ℝ^{} <) \leq inf (B ℝ^{} <) \leftrightarrow \forall x \in B inf (A ℝ^{*} <) \leq x)$
31	28 30	mpbird	$⊢ φ \to inf (A ℝ^{} <) \leq inf (B ℝ^{} <)$

Metamath Proof Explorer

Theorem infleinf2

Proof