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 imbitrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≠ 𝐵 → ¬ ∀ 𝑥 ∈ ℚ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) )
19 18 necon4ad ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ℚ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) → 𝐴 = 𝐵 ) )
20 2 19 impbid2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ ℚ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) )