Metamath Proof Explorer


Theorem xrleid

Description: 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrleid ( 𝐴 ∈ ℝ*𝐴𝐴 )

Proof

Step Hyp Ref Expression
1 eqid 𝐴 = 𝐴
2 1 olci ( 𝐴 < 𝐴𝐴 = 𝐴 )
3 xrleloe ( ( 𝐴 ∈ ℝ*𝐴 ∈ ℝ* ) → ( 𝐴𝐴 ↔ ( 𝐴 < 𝐴𝐴 = 𝐴 ) ) )
4 2 3 mpbiri ( ( 𝐴 ∈ ℝ*𝐴 ∈ ℝ* ) → 𝐴𝐴 )
5 4 anidms ( 𝐴 ∈ ℝ*𝐴𝐴 )