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 ( 𝐴 ⊆ ℝ → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘 → ( 𝜑𝜓 ) ) ↔ ( ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜑 ) ∧ ∃ 𝑗 ∈ ℝ ∀ 𝑘𝐴 ( 𝑗𝑘𝜓 ) ) ) )