Metamath Proof Explorer


Theorem rexico

Description: Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Assertion rexico ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
2 pnfxr +∞ ∈ ℝ*
3 icossre ( ( 𝐵 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝐵 [,) +∞ ) ⊆ ℝ )
4 1 2 3 sylancl ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 [,) +∞ ) ⊆ ℝ )
5 ssrexv ( ( 𝐵 [,) +∞ ) ⊆ ℝ → ( ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ) )
6 4 5 syl ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ) )
7 simpr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → 𝑗 ∈ ℝ )
8 simplr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → 𝐵 ∈ ℝ )
9 7 8 ifcld ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ℝ )
10 max1 ( ( 𝐵 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → 𝐵 ≤ if ( 𝐵𝑗 , 𝑗 , 𝐵 ) )
11 10 adantll ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → 𝐵 ≤ if ( 𝐵𝑗 , 𝑗 , 𝐵 ) )
12 elicopnf ( 𝐵 ∈ ℝ → ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ( 𝐵 [,) +∞ ) ↔ ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ℝ ∧ 𝐵 ≤ if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ) ) )
13 12 ad2antlr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ( 𝐵 [,) +∞ ) ↔ ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ℝ ∧ 𝐵 ≤ if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ) ) )
14 9 11 13 mpbir2and ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ( 𝐵 [,) +∞ ) )
15 simpllr ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℝ )
16 simplr ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝑗 ∈ ℝ )
17 simpll ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → 𝐴 ⊆ ℝ )
18 17 sselda ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ 𝑘𝐴 ) → 𝑘 ∈ ℝ )
19 maxle ( ( 𝐵 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘 ↔ ( 𝐵𝑘𝑗𝑘 ) ) )
20 15 16 18 19 syl3anc ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ 𝑘𝐴 ) → ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘 ↔ ( 𝐵𝑘𝑗𝑘 ) ) )
21 simpr ( ( 𝐵𝑘𝑗𝑘 ) → 𝑗𝑘 )
22 20 21 syl6bi ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ 𝑘𝐴 ) → ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘𝑗𝑘 ) )
23 22 imim1d ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) ∧ 𝑘𝐴 ) → ( ( 𝑗𝑘𝜑 ) → ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘𝜑 ) ) )
24 23 ralimdva ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → ( ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) → ∀ 𝑘𝐴 ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘𝜑 ) ) )
25 breq1 ( 𝑛 = if ( 𝐵𝑗 , 𝑗 , 𝐵 ) → ( 𝑛𝑘 ↔ if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘 ) )
26 25 rspceaimv ( ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ∈ ( 𝐵 [,) +∞ ) ∧ ∀ 𝑘𝐴 ( if ( 𝐵𝑗 , 𝑗 , 𝐵 ) ≤ 𝑘𝜑 ) ) → ∃ 𝑛 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑛𝑘𝜑 ) )
27 14 24 26 syl6an ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑗 ∈ ℝ ) → ( ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) → ∃ 𝑛 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑛𝑘𝜑 ) ) )
28 27 rexlimdva ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) → ∃ 𝑛 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑛𝑘𝜑 ) ) )
29 breq1 ( 𝑛 = 𝑗 → ( 𝑛𝑘𝑗𝑘 ) )
30 29 imbi1d ( 𝑛 = 𝑗 → ( ( 𝑛𝑘𝜑 ) ↔ ( 𝑗𝑘𝜑 ) ) )
31 30 ralbidv ( 𝑛 = 𝑗 → ( ∀ 𝑘𝐴 ( 𝑛𝑘𝜑 ) ↔ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ) )
32 31 cbvrexvw ( ∃ 𝑛 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑛𝑘𝜑 ) ↔ ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) )
33 28 32 syl6ib ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) → ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ) )
34 6 33 impbid ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ) )