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	⊢ Ⅎ 𝑥 𝜑
	infrnmptle.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ^* )
	infrnmptle.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ^* )
	infrnmptle.l	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion	infrnmptle	⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ^* , < ) ≤ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) , ℝ^* , < ) )

Proof

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

Metamath Proof Explorer

Theorem infrnmptle

Proof