Metamath Proof Explorer

Theorem rexabslelem

Description: An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rexabslelem.1 ⊢ Ⅎ 𝑥 𝜑
rexabslelem.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion rexabslelem ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rexabslelem.1 ⊢ Ⅎ 𝑥 𝜑
2 rexabslelem.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
4 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ ℝ
5 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦
6 1 4 5 nf3an ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
7 2 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
8 2 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
9 8 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
10 9 abscld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
11 3 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
12 7 leabsd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ ( abs ‘ 𝐵 ) )
13 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ≤ 𝑦 )
14 13 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ≤ 𝑦 )
15 7 10 11 12 14 letrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
16 15 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 𝑥 ∈ 𝐴 → 𝐵 ≤ 𝑦 ) )
17 6 16 ralrimi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
18 brralrspcev ⊢ ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 )
19 3 17 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 )
20 3 renegcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → - 𝑦 ∈ ℝ )
21 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
22 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
23 absle ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( - 𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦 ) ) )
24 21 22 23 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( - 𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦 ) ) )
25 24 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( - 𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦 ) ) )
26 14 25 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑦 ≤ 𝐵 ∧ 𝐵 ≤ 𝑦 ) )
27 26 simpld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → - 𝑦 ≤ 𝐵 )
28 27 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 𝑥 ∈ 𝐴 → - 𝑦 ≤ 𝐵 ) )
29 6 28 ralrimi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 - 𝑦 ≤ 𝐵 )
30 breq1 ⊢ ( 𝑧 = - 𝑦 → ( 𝑧 ≤ 𝐵 ↔ - 𝑦 ≤ 𝐵 ) )
31 30 ralbidv ⊢ ( 𝑧 = - 𝑦 → ( ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 - 𝑦 ≤ 𝐵 ) )
32 31 rspcev ⊢ ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 - 𝑦 ≤ 𝐵 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 )
33 20 29 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 )
34 19 33 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) )
35 34 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) ) )
36 35 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )
37 renegcl ⊢ ( 𝑧 ∈ ℝ → - 𝑧 ∈ ℝ )
38 37 adantl ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - 𝑧 ∈ ℝ )
39 simpl ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑤 ∈ ℝ )
40 38 39 ifcld ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
41 40 ad5ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
42 nfv ⊢ Ⅎ 𝑥 𝑤 ∈ ℝ
43 1 42 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ ℝ )
44 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤
45 43 44 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 )
46 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ ℝ
47 45 46 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ )
48 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵
49 47 48 nfan ⊢ Ⅎ 𝑥 ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 )
50 40 ad5ant23 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
51 50 renegcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
52 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
53 2 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
54 max2 ⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑧 ∈ ℝ ) → - 𝑧 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
55 39 38 54 syl2anc ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - 𝑧 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
56 38 40 lenegd ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( - 𝑧 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ↔ - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ - - 𝑧 ) )
57 55 56 mpbid ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ - - 𝑧 )
58 recn ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℂ )
59 58 adantl ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℂ )
60 59 negnegd ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - - 𝑧 = 𝑧 )
61 57 60 breqtrd ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝑧 )
62 61 ad5ant23 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝑧 )
63 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ≤ 𝐵 )
64 63 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ≤ 𝐵 )
65 51 52 53 62 64 letrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 )
66 65 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 )
67 2 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
68 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑤 ∈ ℝ )
69 40 ad5ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
70 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑤 )
71 70 ad4ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑤 )
72 max1 ⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑧 ∈ ℝ ) → 𝑤 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
73 39 38 72 syl2anc ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑤 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
74 73 ad5ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑤 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
75 67 68 69 71 74 letrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
76 75 adantlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
77 66 76 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 ∧ 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) )
78 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
79 78 3adant2 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
80 40 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
81 80 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
82 79 81 absled ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ↔ ( - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 ∧ 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) ) )
83 82 ad5ant135 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ↔ ( - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 ∧ 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) ) )
84 77 83 mpbird ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
85 84 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) )
86 49 85 ralrimi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
87 brralrspcev ⊢ ( ( if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
88 41 86 87 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
89 88 exp31 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) → ( 𝑧 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) )
90 89 exp31 ⊢ ( 𝜑 → ( 𝑤 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 → ( 𝑧 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) ) )
91 90 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 → ( 𝑧 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) )
92 91 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) → ( 𝑧 ∈ ℝ → ( ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) )
93 92 rexlimdv ⊢ ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) → ( ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
94 93 imp ⊢ ( ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
95 94 anasss ⊢ ( ( 𝜑 ∧ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
96 95 ex ⊢ ( 𝜑 → ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
97 36 96 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑧 ≤ 𝐵 ) ) )