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 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∃ 𝑗 ∈ ( 𝐵 [,) +∞ ) ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ) )