infrnmptle

Description: An indexed infimum of extended reals is smaller than another indexed infimum of extended reals, when every indexed element is smaller than the corresponding one. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	infrnmptle.x	$⊢ Ⅎ x φ$
	infrnmptle.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
	infrnmptle.c	$⊢ (φ \land x \in A) \to C \in ℝ^{*}$
	infrnmptle.l	$⊢ (φ \land x \in A) \to B \leq C$
Assertion	infrnmptle	$⊢ φ \to inf (ran (x \in A ⟼ B) ℝ^{} <) \leq inf (ran (x \in A ⟼ C) ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		infrnmptle.x	$⊢ Ⅎ x φ$
2		infrnmptle.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
3		infrnmptle.c	$⊢ (φ \land x \in A) \to C \in ℝ^{*}$
4		infrnmptle.l	$⊢ (φ \land x \in A) \to B \leq C$
5		nfv	$⊢ Ⅎ y φ$
6		nfv	$⊢ Ⅎ z φ$
7		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
8	1 7 2	rnmptssd	$⊢ φ \to ran (x \in A ⟼ B) \subseteq ℝ^{*}$
9		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
10	1 9 3	rnmptssd	$⊢ φ \to ran (x \in A ⟼ C) \subseteq ℝ^{*}$
11		vex	$⊢ y \in V$
12	9	elrnmpt	$⊢ y \in V \to (y \in ran (x \in A ⟼ C) \leftrightarrow \exists x \in A y = C)$
13	11 12	ax-mp	$⊢ y \in ran (x \in A ⟼ C) \leftrightarrow \exists x \in A y = C$
14	13	bilani	$⊢ (φ \land y \in ran (x \in A ⟼ C)) \to \exists x \in A y = C$
15		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
16	15	nfrn	$⊢ \underline{Ⅎ} x ran (x \in A ⟼ B)$
17		nfv	$⊢ Ⅎ x z \leq y$
18	16 17	nfrexw	$⊢ Ⅎ x \exists z \in ran (x \in A ⟼ B) z \leq y$
19		simpr	$⊢ (φ \land x \in A) \to x \in A$
20	7	elrnmpt1	$⊢ (x \in A \land B \in ℝ^{*}) \to B \in ran (x \in A ⟼ B)$
21	19 2 20	syl2anc	$⊢ (φ \land x \in A) \to B \in ran (x \in A ⟼ B)$
22	21	3adant3	$⊢ (φ \land x \in A \land y = C) \to B \in ran (x \in A ⟼ B)$
23	4	3adant3	$⊢ (φ \land x \in A \land y = C) \to B \leq C$
24		id	$⊢ y = C \to y = C$
25	24	eqcomd	$⊢ y = C \to C = y$
26	25	3ad2ant3	$⊢ (φ \land x \in A \land y = C) \to C = y$
27	23 26	breqtrd	$⊢ (φ \land x \in A \land y = C) \to B \leq y$
28		breq1	$⊢ z = B \to (z \leq y \leftrightarrow B \leq y)$
29	28	rspcev	$⊢ (B \in ran (x \in A ⟼ B) \land B \leq y) \to \exists z \in ran (x \in A ⟼ B) z \leq y$
30	22 27 29	syl2anc	$⊢ (φ \land x \in A \land y = C) \to \exists z \in ran (x \in A ⟼ B) z \leq y$
31	30	3exp	$⊢ φ \to (x \in A \to (y = C \to \exists z \in ran (x \in A ⟼ B) z \leq y))$
32	1 18 31	rexlimd	$⊢ φ \to (\exists x \in A y = C \to \exists z \in ran (x \in A ⟼ B) z \leq y)$
33	32	adantr	$⊢ (φ \land y \in ran (x \in A ⟼ C)) \to (\exists x \in A y = C \to \exists z \in ran (x \in A ⟼ B) z \leq y)$
34	14 33	mpd	$⊢ (φ \land y \in ran (x \in A ⟼ C)) \to \exists z \in ran (x \in A ⟼ B) z \leq y$
35	5 6 8 10 34	infleinf2	$⊢ φ \to inf (ran (x \in A ⟼ B) ℝ^{} <) \leq inf (ran (x \in A ⟼ C) ℝ^{} <)$

Metamath Proof Explorer

Theorem infrnmptle

Proof