Metamath Proof Explorer

Theorem rexanre

Description: Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016)

Ref Expression
Assertion rexanre ( 𝐴 ⊆ ℝ → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
2 1 imim2i ⊢ ( ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ( 𝑗 ≤ 𝑘 → 𝜑 ) )
3 2 ralimi ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) )
4 3 reximi ⊢ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) )
5 simpr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
6 5 imim2i ⊢ ( ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ( 𝑗 ≤ 𝑘 → 𝜓 ) )
7 6 ralimi ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) )
8 7 reximi ⊢ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) )
9 4 8 jca ⊢ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ) )
10 breq1 ⊢ ( 𝑗 = 𝑥 → ( 𝑗 ≤ 𝑘 ↔ 𝑥 ≤ 𝑘 ) )
11 10 imbi1d ⊢ ( 𝑗 = 𝑥 → ( ( 𝑗 ≤ 𝑘 → 𝜑 ) ↔ ( 𝑥 ≤ 𝑘 → 𝜑 ) ) )
12 11 ralbidv ⊢ ( 𝑗 = 𝑥 → ( ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ) )
13 12 cbvrexvw ⊢ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) )
14 breq1 ⊢ ( 𝑗 = 𝑦 → ( 𝑗 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘 ) )
15 14 imbi1d ⊢ ( 𝑗 = 𝑦 → ( ( 𝑗 ≤ 𝑘 → 𝜓 ) ↔ ( 𝑦 ≤ 𝑘 → 𝜓 ) ) )
16 15 ralbidv ⊢ ( 𝑗 = 𝑦 → ( ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) )
17 16 cbvrexvw ⊢ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) )
18 13 17 anbi12i ⊢ ( ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) )
19 reeanv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) )
20 18 19 bitr4i ⊢ ( ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) )
21 ifcl ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℝ )
22 21 ancoms ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℝ )
23 22 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℝ )
24 r19.26 ⊢ ( ∀ 𝑘 ∈ 𝐴 ( ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ( 𝑦 ≤ 𝑘 → 𝜓 ) ) ↔ ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) )
25 anim12 ⊢ ( ( ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ( 𝑦 ≤ 𝑘 → 𝜓 ) ) → ( ( 𝑥 ≤ 𝑘 ∧ 𝑦 ≤ 𝑘 ) → ( 𝜑 ∧ 𝜓 ) ) )
26 simplrl ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
27 simplrr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
28 simpl ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
29 28 sselda ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ℝ )
30 maxle ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 ↔ ( 𝑥 ≤ 𝑘 ∧ 𝑦 ≤ 𝑘 ) ) )
31 26 27 29 30 syl3anc ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑘 ∈ 𝐴 ) → ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 ↔ ( 𝑥 ≤ 𝑘 ∧ 𝑦 ≤ 𝑘 ) ) )
32 31 imbi1d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑥 ≤ 𝑘 ∧ 𝑦 ≤ 𝑘 ) → ( 𝜑 ∧ 𝜓 ) ) ) )
33 25 32 syl5ibr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ( 𝑦 ≤ 𝑘 → 𝜓 ) ) → ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) )
34 33 ralimdva ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ∀ 𝑘 ∈ 𝐴 ( ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ( 𝑦 ≤ 𝑘 → 𝜓 ) ) → ∀ 𝑘 ∈ 𝐴 ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) )
35 24 34 syl5bir ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) → ∀ 𝑘 ∈ 𝐴 ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) )
36 breq1 ⊢ ( 𝑗 = if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) → ( 𝑗 ≤ 𝑘 ↔ if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 ) )
37 36 rspceaimv ⊢ ( ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ∈ ℝ ∧ ∀ 𝑘 ∈ 𝐴 ( if ( 𝑥 ≤ 𝑦 , 𝑦 , 𝑥 ) ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) )
38 23 35 37 syl6an ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) )
39 38 rexlimdvva ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ ( ∀ 𝑘 ∈ 𝐴 ( 𝑥 ≤ 𝑘 → 𝜑 ) ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑦 ≤ 𝑘 → 𝜓 ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) )
40 20 39 syl5bi ⊢ ( 𝐴 ⊆ ℝ → ( ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ) → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ) )
41 9 40 impbid2 ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝐴 ( 𝑗 ≤ 𝑘 → 𝜓 ) ) ) )