Step | Hyp | Ref
| Expression |
1 | | elicc1 9828 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 ∈ (𝐴[,]𝐴) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
2 | 1 | anidms 395 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈ (𝐴[,]𝐴) ↔ (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
3 | | xrlenlt 7942 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐴 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐴)) |
4 | | xrlenlt 7942 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
5 | 4 | ancoms 266 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑥 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑥)) |
6 | | xrlttri3 9704 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → (𝑥 = 𝐴 ↔ (¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥))) |
7 | 6 | biimprd 157 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝐴 ∈
ℝ*) → ((¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥) → 𝑥 = 𝐴)) |
8 | 7 | ancoms 266 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → ((¬ 𝑥 < 𝐴 ∧ ¬ 𝐴 < 𝑥) → 𝑥 = 𝐴)) |
9 | 8 | expcomd 1421 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (¬ 𝐴 < 𝑥 → (¬ 𝑥 < 𝐴 → 𝑥 = 𝐴))) |
10 | 5, 9 | sylbid 149 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑥 ≤ 𝐴 → (¬ 𝑥 < 𝐴 → 𝑥 = 𝐴))) |
11 | 10 | com23 78 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (¬ 𝑥 < 𝐴 → (𝑥 ≤ 𝐴 → 𝑥 = 𝐴))) |
12 | 3, 11 | sylbid 149 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝐴 ≤ 𝑥 → (𝑥 ≤ 𝐴 → 𝑥 = 𝐴))) |
13 | 12 | ex 114 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈
ℝ* → (𝐴 ≤ 𝑥 → (𝑥 ≤ 𝐴 → 𝑥 = 𝐴)))) |
14 | 13 | 3impd 1203 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐴) → 𝑥 = 𝐴)) |
15 | | eleq1a 2229 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → 𝑥 ∈
ℝ*)) |
16 | | xrleid 9707 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ 𝐴 ≤ 𝐴) |
17 | | breq2 3969 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐴 ≤ 𝑥 ↔ 𝐴 ≤ 𝐴)) |
18 | 16, 17 | syl5ibrcom 156 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → 𝐴 ≤ 𝑥)) |
19 | | breq1 3968 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 ≤ 𝐴 ↔ 𝐴 ≤ 𝐴)) |
20 | 16, 19 | syl5ibrcom 156 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → 𝑥 ≤ 𝐴)) |
21 | 15, 18, 20 | 3jcad 1163 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (𝑥 = 𝐴 → (𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐴))) |
22 | 14, 21 | impbid 128 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐴) ↔ 𝑥 = 𝐴)) |
23 | | velsn 3577 |
. . . 4
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
24 | 22, 23 | bitr4di 197 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ ((𝑥 ∈
ℝ* ∧ 𝐴
≤ 𝑥 ∧ 𝑥 ≤ 𝐴) ↔ 𝑥 ∈ {𝐴})) |
25 | 2, 24 | bitrd 187 |
. 2
⊢ (𝐴 ∈ ℝ*
→ (𝑥 ∈ (𝐴[,]𝐴) ↔ 𝑥 ∈ {𝐴})) |
26 | 25 | eqrdv 2155 |
1
⊢ (𝐴 ∈ ℝ*
→ (𝐴[,]𝐴) = {𝐴}) |