Step | Hyp | Ref
| Expression |
1 | | elicc1 8947 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 ∈ (𝐴[,]𝐴) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
2 | 1 | anidms 389 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈ (𝐴[,]𝐴) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
3 | | xrlenlt 7177 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐴 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐴)) |
4 | | xrlenlt 7177 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
5 | 4 | ancoms 264 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
6 | | xrlttri3 8872 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 = 𝐴 ↔ (¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥))) |
7 | 6 | biimprd 156 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → ((¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥) → 𝑥 = 𝐴)) |
8 | 7 | ancoms 264 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → ((¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥) → 𝑥 = 𝐴)) |
9 | 8 | expcomd 1370 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (¬ 𝐴 < 𝑥 → (¬ 𝑥 < 𝐴 → 𝑥 = 𝐴))) |
10 | 5, 9 | sylbid 148 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑥 ≤ 𝐴 → (¬ 𝑥 < 𝐴 → 𝑥 = 𝐴))) |
11 | 10 | com23 77 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (¬ 𝑥 < 𝐴 → (𝑥 ≤ 𝐴 → 𝑥 = 𝐴))) |
12 | 3, 11 | sylbid 148 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐴 ≤ 𝑥 → (𝑥 ≤ 𝐴 → 𝑥 = 𝐴))) |
13 | 12 | ex 113 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈
ℝ* → (𝐴 ≤ 𝑥 → (𝑥 ≤ 𝐴 → 𝑥 = 𝐴)))) |
14 | 13 | 3impd 1152 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐴) → 𝑥 = 𝐴)) |
15 | | eleq1a 2150 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → 𝑥 ∈
ℝ*)) |
16 | | xrleid 8874 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤ 𝐴) |
17 | | breq2 3789 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐴)) |
18 | 16, 17 | syl5ibrcom 155 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → 𝐴 ≤ 𝑥)) |
19 | | breq1 3788 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ≤ 𝐴 ↔ 𝐴 ≤ 𝐴)) |
20 | 16, 19 | syl5ibrcom 155 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → 𝑥 ≤ 𝐴)) |
21 | 15, 18, 20 | 3jcad 1119 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
22 | 14, 21 | impbid 127 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐴) ↔ 𝑥 = 𝐴)) |
23 | | velsn 3415 |
. . . 4
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
24 | 22, 23 | syl6bbr 196 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐴) ↔ 𝑥 ∈ {𝐴})) |
25 | 2, 24 | bitrd 186 |
. 2
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈ (𝐴[,]𝐴) ↔ 𝑥 ∈ {𝐴})) |
26 | 25 | eqrdv 2079 |
1
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |