Metamath Proof Explorer


Theorem qextle

Description: An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion qextle ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ ℚ ( 𝑥𝐴𝑥𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝐴 = 𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
2 1 ralrimivw ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ ℚ ( 𝑥𝐴𝑥𝐵 ) )
3 xrlttri2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴𝐵 ↔ ( 𝐴 < 𝐵𝐵 < 𝐴 ) ) )
4 qextltlem ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐴𝑥 < 𝐵 ) ∧ ¬ ( 𝑥𝐴𝑥𝐵 ) ) ) )
5 simpr ( ( ¬ ( 𝑥 < 𝐴𝑥 < 𝐵 ) ∧ ¬ ( 𝑥𝐴𝑥𝐵 ) ) → ¬ ( 𝑥𝐴𝑥𝐵 ) )
6 5 reximi ( ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐴𝑥 < 𝐵 ) ∧ ¬ ( 𝑥𝐴𝑥𝐵 ) ) → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) )
7 4 6 syl6 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) ) )
8 qextltlem ( ( 𝐵 ∈ ℝ*𝐴 ∈ ℝ* ) → ( 𝐵 < 𝐴 → ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐵𝑥 < 𝐴 ) ∧ ¬ ( 𝑥𝐵𝑥𝐴 ) ) ) )
9 simpr ( ( ¬ ( 𝑥 < 𝐵𝑥 < 𝐴 ) ∧ ¬ ( 𝑥𝐵𝑥𝐴 ) ) → ¬ ( 𝑥𝐵𝑥𝐴 ) )
10 bicom ( ( 𝑥𝐵𝑥𝐴 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
11 9 10 sylnib ( ( ¬ ( 𝑥 < 𝐵𝑥 < 𝐴 ) ∧ ¬ ( 𝑥𝐵𝑥𝐴 ) ) → ¬ ( 𝑥𝐴𝑥𝐵 ) )
12 11 reximi ( ∃ 𝑥 ∈ ℚ ( ¬ ( 𝑥 < 𝐵𝑥 < 𝐴 ) ∧ ¬ ( 𝑥𝐵𝑥𝐴 ) ) → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) )
13 8 12 syl6 ( ( 𝐵 ∈ ℝ*𝐴 ∈ ℝ* ) → ( 𝐵 < 𝐴 → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) ) )
14 13 ancoms ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐵 < 𝐴 → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) ) )
15 7 14 jaod ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 < 𝐵𝐵 < 𝐴 ) → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) ) )
16 3 15 sylbid ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴𝐵 → ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) ) )
17 rexnal ( ∃ 𝑥 ∈ ℚ ¬ ( 𝑥𝐴𝑥𝐵 ) ↔ ¬ ∀ 𝑥 ∈ ℚ ( 𝑥𝐴𝑥𝐵 ) )
18 16 17 syl6ib ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴𝐵 → ¬ ∀ 𝑥 ∈ ℚ ( 𝑥𝐴𝑥𝐵 ) ) )
19 18 necon4ad ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℚ ( 𝑥𝐴𝑥𝐵 ) → 𝐴 = 𝐵 ) )
20 2 19 impbid2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ ℚ ( 𝑥𝐴𝑥𝐵 ) ) )