Metamath Proof Explorer

Theorem qextlt

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

Ref Expression
Assertion qextlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ ∀ x ∈ ℚ x < A ↔ x < B

Proof

Step Hyp Ref Expression
1 breq2 ⊢ A = B → x < A ↔ x < B
2 1 ralrimivw ⊢ A = B → ∀ x ∈ ℚ x < A ↔ x < B
3 xrlttri2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≠ B ↔ A < B ∨ B < A
4 qextltlem ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B → ∃ x ∈ ℚ ¬ x < A ↔ x < B ∧ ¬ x ≤ A ↔ x ≤ B
5 simpl ⊢ ¬ x < A ↔ x < B ∧ ¬ x ≤ A ↔ x ≤ B → ¬ x < A ↔ x < B
6 5 reximi ⊢ ∃ x ∈ ℚ ¬ x < A ↔ x < B ∧ ¬ x ≤ A ↔ x ≤ B → ∃ x ∈ ℚ ¬ x < A ↔ x < B
7 4 6 syl6 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B → ∃ x ∈ ℚ ¬ x < A ↔ x < B
8 qextltlem ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B < A → ∃ x ∈ ℚ ¬ x < B ↔ x < A ∧ ¬ x ≤ B ↔ x ≤ A
9 simpl ⊢ ¬ x < B ↔ x < A ∧ ¬ x ≤ B ↔ x ≤ A → ¬ x < B ↔ x < A
10 bicom ⊢ x < B ↔ x < A ↔ x < A ↔ x < B
11 9 10 sylnib ⊢ ¬ x < B ↔ x < A ∧ ¬ x ≤ B ↔ x ≤ A → ¬ x < A ↔ x < B
12 11 reximi ⊢ ∃ x ∈ ℚ ¬ x < B ↔ x < A ∧ ¬ x ≤ B ↔ x ≤ A → ∃ x ∈ ℚ ¬ x < A ↔ x < B
13 8 12 syl6 ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B < A → ∃ x ∈ ℚ ¬ x < A ↔ x < B
14 13 ancoms ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B < A → ∃ x ∈ ℚ ¬ x < A ↔ x < B
15 7 14 jaod ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ∨ B < A → ∃ x ∈ ℚ ¬ x < A ↔ x < B
16 3 15 sylbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≠ B → ∃ x ∈ ℚ ¬ x < A ↔ x < B
17 rexnal ⊢ ∃ x ∈ ℚ ¬ x < A ↔ x < B ↔ ¬ ∀ x ∈ ℚ x < A ↔ x < B
18 16 17 syl6ib ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≠ B → ¬ ∀ x ∈ ℚ x < A ↔ x < B
19 18 necon4ad ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ∀ x ∈ ℚ x < A ↔ x < B → A = B
20 2 19 impbid2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ ∀ x ∈ ℚ x < A ↔ x < B