Metamath Proof Explorer

Theorem 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 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
infrnmptle.c ⊢ φ ∧ x ∈ A → C ∈ ℝ *
infrnmptle.l ⊢ φ ∧ x ∈ A → B ≤ C
Assertion infrnmptle ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ * < ≤ inf ran ⁡ x ∈ A ⟼ C ℝ * <

Proof

Step Hyp Ref Expression
1 infrnmptle.x ⊢ Ⅎ x φ
2 infrnmptle.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
3 infrnmptle.c ⊢ φ ∧ x ∈ A → C ∈ ℝ *
4 infrnmptle.l ⊢ φ ∧ x ∈ A → B ≤ C
5 nfv ⊢ Ⅎ y φ
6 nfv ⊢ Ⅎ z φ
7 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
8 1 7 2 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ B ⊆ ℝ *
9 eqid ⊢ x ∈ A ⟼ C = x ∈ A ⟼ C
10 1 9 3 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ C ⊆ ℝ *
11 vex ⊢ y ∈ V
12 9 elrnmpt ⊢ y ∈ V → y ∈ ran ⁡ x ∈ A ⟼ C ↔ ∃ x ∈ A y = C
13 11 12 ax-mp ⊢ y ∈ ran ⁡ x ∈ A ⟼ C ↔ ∃ x ∈ A y = C
14 13 biimpi ⊢ y ∈ ran ⁡ x ∈ A ⟼ C → ∃ x ∈ A y = C
15 14 adantl ⊢ φ ∧ y ∈ ran ⁡ x ∈ A ⟼ C → ∃ x ∈ A y = C
16 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
17 16 nfrn ⊢ Ⅎ _ x ran ⁡ x ∈ A ⟼ B
18 nfv ⊢ Ⅎ x z ≤ y
19 17 18 nfrexw ⊢ Ⅎ x ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
20 simpr ⊢ φ ∧ x ∈ A → x ∈ A
21 7 elrnmpt1 ⊢ x ∈ A ∧ B ∈ ℝ * → B ∈ ran ⁡ x ∈ A ⟼ B
22 20 2 21 syl2anc ⊢ φ ∧ x ∈ A → B ∈ ran ⁡ x ∈ A ⟼ B
23 22 3adant3 ⊢ φ ∧ x ∈ A ∧ y = C → B ∈ ran ⁡ x ∈ A ⟼ B
24 4 3adant3 ⊢ φ ∧ x ∈ A ∧ y = C → B ≤ C
25 id ⊢ y = C → y = C
26 25 eqcomd ⊢ y = C → C = y
27 26 3ad2ant3 ⊢ φ ∧ x ∈ A ∧ y = C → C = y
28 24 27 breqtrd ⊢ φ ∧ x ∈ A ∧ y = C → B ≤ y
29 breq1 ⊢ z = B → z ≤ y ↔ B ≤ y
30 29 rspcev ⊢ B ∈ ran ⁡ x ∈ A ⟼ B ∧ B ≤ y → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
31 23 28 30 syl2anc ⊢ φ ∧ x ∈ A ∧ y = C → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
32 31 3exp ⊢ φ → x ∈ A → y = C → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
33 1 19 32 rexlimd ⊢ φ → ∃ x ∈ A y = C → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
34 33 adantr ⊢ φ ∧ y ∈ ran ⁡ x ∈ A ⟼ C → ∃ x ∈ A y = C → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
35 15 34 mpd ⊢ φ ∧ y ∈ ran ⁡ x ∈ A ⟼ C → ∃ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
36 5 6 8 10 35 infleinf2 ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ * < ≤ inf ran ⁡ x ∈ A ⟼ C ℝ * <