Database
BASIC ORDER THEORY
Posets, directed sets, and lattices as relations
Posets and lattices as relations
lefld
Metamath Proof Explorer
Description: The field of the 'less or equal to' relationship on the extended real.
(Contributed by FL , 2-Aug-2009) (Revised by Mario Carneiro , 4-May-2015)
Ref
Expression
Assertion
lefld
⊢ ℝ* = ∪ ∪ ≤
Proof
Step
Hyp
Ref
Expression
1
lerel
⊢ Rel ≤
2
relfld
⊢ ( Rel ≤ → ∪ ∪ ≤ = ( dom ≤ ∪ ran ≤ ) )
3
1 2
ax-mp
⊢ ∪ ∪ ≤ = ( dom ≤ ∪ ran ≤ )
4
ledm
⊢ ℝ* = dom ≤
5
lern
⊢ ℝ* = ran ≤
6
4 5
uneq12i
⊢ ( ℝ* ∪ ℝ* ) = ( dom ≤ ∪ ran ≤ )
7
unidm
⊢ ( ℝ* ∪ ℝ* ) = ℝ*
8
3 6 7
3eqtr2ri
⊢ ℝ* = ∪ ∪ ≤