Theorem lerelxr 11206

Description: "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
lerelxr	⊢ ≤ ⊆ (ℝ* × ℝ*)

Proof of Theorem lerelxr

Step	Hyp	Ref	Expression
1		df-le 11183	. 2 ⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < )
2		difss 4073	. 2 ⊢ ((ℝ* × ℝ*) ∖ ◡ < ) ⊆ (ℝ* × ℝ*)
3	1, 2	eqsstri 3968	1 ⊢ ≤ ⊆ (ℝ* × ℝ*)

Syntax hints:   ∖ cdif 3887   ⊆ wss 3890   × cxp 5623  ^◡ccnv 5624  ℝ^*cxr 11176   < clt 11177   ≤ cle 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907  df-le 11183

This theorem is referenced by:  lerel  11207  dfle2  13096  dflt2  13097  xrsle  17566  ledm  18554  lern  18555  letsr  18557  znle  21518  leex  42737  i0oii  49417  io1ii  49418