Step | Hyp | Ref
| Expression |
1 | | elicc1 8563 |
. . . 4
⊢
((A ∈ ℝ* ∧ A ∈ ℝ*) → (x ∈ (A[,]A) ↔
(x ∈
ℝ* ∧ A ≤ x ∧ x ≤
A))) |
2 | 1 | anidms 377 |
. . 3
⊢ (A ∈
ℝ* → (x ∈ (A[,]A) ↔ (x
∈ ℝ* ∧ A ≤
x ∧
x ≤ A))) |
3 | | xrlenlt 6881 |
. . . . . . . 8
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → (A ≤ x ↔
¬ x < A)) |
4 | | xrlenlt 6881 |
. . . . . . . . . . 11
⊢
((x ∈ ℝ* ∧ A ∈ ℝ*) → (x ≤ A ↔
¬ A < x)) |
5 | 4 | ancoms 255 |
. . . . . . . . . 10
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → (x ≤ A ↔
¬ A < x)) |
6 | | xrlttri3 8488 |
. . . . . . . . . . . . 13
⊢
((x ∈ ℝ* ∧ A ∈ ℝ*) → (x = A ↔
(¬ x < A ∧ ¬ A < x))) |
7 | 6 | biimprd 147 |
. . . . . . . . . . . 12
⊢
((x ∈ ℝ* ∧ A ∈ ℝ*) → ((¬ x < A ∧ ¬ A <
x) → x = A)) |
8 | 7 | ancoms 255 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → ((¬ x < A ∧ ¬ A <
x) → x = A)) |
9 | 8 | expcomd 1327 |
. . . . . . . . . 10
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → (¬ A < x →
(¬ x < A → x =
A))) |
10 | 5, 9 | sylbid 139 |
. . . . . . . . 9
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → (x ≤ A →
(¬ x < A → x =
A))) |
11 | 10 | com23 72 |
. . . . . . . 8
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → (¬ x < A →
(x ≤ A → x =
A))) |
12 | 3, 11 | sylbid 139 |
. . . . . . 7
⊢
((A ∈ ℝ* ∧ x ∈ ℝ*) → (A ≤ x →
(x ≤ A → x =
A))) |
13 | 12 | ex 108 |
. . . . . 6
⊢ (A ∈
ℝ* → (x ∈ ℝ* → (A ≤ x →
(x ≤ A → x =
A)))) |
14 | 13 | 3impd 1117 |
. . . . 5
⊢ (A ∈
ℝ* → ((x ∈ ℝ* ∧ A ≤
x ∧
x ≤ A) → x =
A)) |
15 | | eleq1a 2106 |
. . . . . 6
⊢ (A ∈
ℝ* → (x = A → x ∈ ℝ*)) |
16 | | xrleid 8490 |
. . . . . . 7
⊢ (A ∈
ℝ* → A ≤ A) |
17 | | breq2 3759 |
. . . . . . 7
⊢ (x = A →
(A ≤ x ↔ A ≤
A)) |
18 | 16, 17 | syl5ibrcom 146 |
. . . . . 6
⊢ (A ∈
ℝ* → (x = A → A ≤
x)) |
19 | | breq1 3758 |
. . . . . . 7
⊢ (x = A →
(x ≤ A ↔ A ≤
A)) |
20 | 16, 19 | syl5ibrcom 146 |
. . . . . 6
⊢ (A ∈
ℝ* → (x = A → x ≤
A)) |
21 | 15, 18, 20 | 3jcad 1084 |
. . . . 5
⊢ (A ∈
ℝ* → (x = A → (x
∈ ℝ* ∧ A ≤
x ∧
x ≤ A))) |
22 | 14, 21 | impbid 120 |
. . . 4
⊢ (A ∈
ℝ* → ((x ∈ ℝ* ∧ A ≤
x ∧
x ≤ A) ↔ x =
A)) |
23 | | elsn 3382 |
. . . 4
⊢ (x ∈ {A} ↔ x =
A) |
24 | 22, 23 | syl6bbr 187 |
. . 3
⊢ (A ∈
ℝ* → ((x ∈ ℝ* ∧ A ≤
x ∧
x ≤ A) ↔ x
∈ {A})) |
25 | 2, 24 | bitrd 177 |
. 2
⊢ (A ∈
ℝ* → (x ∈ (A[,]A) ↔ x
∈ {A})) |
26 | 25 | eqrdv 2035 |
1
⊢ (A ∈
ℝ* → (A[,]A) = {A}) |