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 ⊢ A ⊆ ℝ ∧ B ∈ ℝ → ∃ j ∈ B +∞ ∀ k ∈ A j ≤ k → φ ↔ ∃ j ∈ ℝ ∀ k ∈ A j ≤ k → φ

Proof

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