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	bilani	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 )
15		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
16	15	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
17		nfv	⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
18	16 17	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦
19		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
20	7	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ^* ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
21	19 2 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22	21	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
23	4	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐵 ≤ 𝐶 )
24		id	⊢ ( 𝑦 = 𝐶 → 𝑦 = 𝐶 )
25	24	eqcomd	⊢ ( 𝑦 = 𝐶 → 𝐶 = 𝑦 )
26	25	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐶 = 𝑦 )
27	23 26	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → 𝐵 ≤ 𝑦 )
28		breq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
29	28	rspcev	⊢ ( ( 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ 𝐵 ≤ 𝑦 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
30	22 27 29	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶 ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
31	30	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐶 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ) )
32	1 18 31	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐶 → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
34	14 33	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) → ∃ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
35	5 6 8 10 34	infleinf2	⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ^* , < ) ≤ inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem infrnmptle

Proof