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