This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supxrleubrnmptf

Description: The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses supxrleubrnmptf.x ⊢ Ⅎ 𝑥 𝜑
supxrleubrnmptf.a ⊢ Ⅎ 𝑥 𝐴
supxrleubrnmptf.n ⊢ Ⅎ 𝑥 𝐶
supxrleubrnmptf.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
supxrleubrnmptf.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion supxrleubrnmptf ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 supxrleubrnmptf.x ⊢ Ⅎ 𝑥 𝜑
2 supxrleubrnmptf.a ⊢ Ⅎ 𝑥 𝐴
3 supxrleubrnmptf.n ⊢ Ⅎ 𝑥 𝐶
4 supxrleubrnmptf.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
5 supxrleubrnmptf.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
6 nfcv ⊢ Ⅎ 𝑦 𝐴
7 nfcv ⊢ Ⅎ 𝑦 𝐵
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10 2 6 7 8 9 cbvmptf ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11 10 rneqi ⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
12 11 supeq1i ⊢ sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < )
13 12 breq1i ⊢ ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < ) ≤ 𝐶 )
14 13 a1i ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ) )
15 nfv ⊢ Ⅎ 𝑦 𝜑
16 2 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
17 1 16 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 )
18 8 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ*
19 17 18 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* )
20 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
21 20 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
22 9 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℝ* ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* ) )
23 21 22 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* ) ) )
24 19 23 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* )
25 15 24 5 supxrleubrnmpt ⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ) )
26 nfcv ⊢ Ⅎ 𝑥 ≤
27 8 26 3 nfbr ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶
28 nfv ⊢ Ⅎ 𝑦 𝐵 ≤ 𝐶
29 eqcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
30 29 imbi1i ⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
31 eqcom ⊢ ( 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
32 31 imbi2i ⊢ ( ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
33 30 32 bitri ⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
34 9 33 mpbi ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
35 34 breq1d ⊢ ( 𝑦 = 𝑥 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶 ) )
36 6 2 27 28 35 cbvralfw ⊢ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
37 36 a1i ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )
38 14 25 37 3bitrd ⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )