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 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ ℚ ( 𝑥 ≤ 𝐴 ↔ 𝑥 ≤ 𝐵 ) ) ) |