![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-rrhat | Structured version Visualization version GIF version |
Description: Define the real projective line. (Contributed by BJ, 27-Jun-2019.) |
Ref | Expression |
---|---|
df-bj-rrhat | ⊢ ℝ̂ = (ℝ ∪ {∞}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crrhat 36622 | . 2 class ℝ̂ | |
2 | cr 11111 | . . 3 class ℝ | |
3 | cinfty 36618 | . . . 4 class ∞ | |
4 | 3 | csn 4623 | . . 3 class {∞} |
5 | 2, 4 | cun 3941 | . 2 class (ℝ ∪ {∞}) |
6 | 1, 5 | wceq 1533 | 1 wff ℝ̂ = (ℝ ∪ {∞}) |
Colors of variables: wff setvar class |
This definition is referenced by: bj-rrhatsscchat 36624 |
Copyright terms: Public domain | W3C validator |