MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  max1ALT Structured version   Unicode version

Theorem max1ALT 11427
Description: A number is less than or equal to the maximum of it and another. This version of max1 11426 omits the  B  e.  RR antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 11426 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.)
Assertion
Ref Expression
max1ALT  |-  ( A  e.  RR  ->  A  <_  if ( A  <_  B ,  B ,  A ) )

Proof of Theorem max1ALT
StepHypRef Expression
1 leid 9675 . . 3  |-  ( A  e.  RR  ->  A  <_  A )
2 iffalse 3858 . . . 4  |-  ( -.  A  <_  B  ->  if ( A  <_  B ,  B ,  A )  =  A )
32breq2d 4373 . . 3  |-  ( -.  A  <_  B  ->  ( A  <_  if ( A  <_  B ,  B ,  A )  <->  A  <_  A ) )
41, 3syl5ibrcom 225 . 2  |-  ( A  e.  RR  ->  ( -.  A  <_  B  ->  A  <_  if ( A  <_  B ,  B ,  A ) ) )
5 id 22 . . 3  |-  ( A  <_  B  ->  A  <_  B )
6 iftrue 3855 . . 3  |-  ( A  <_  B  ->  if ( A  <_  B ,  B ,  A )  =  B )
75, 6breqtrrd 4388 . 2  |-  ( A  <_  B  ->  A  <_  if ( A  <_  B ,  B ,  A ) )
84, 7pm2.61d2 163 1  |-  ( A  e.  RR  ->  A  <_  if ( A  <_  B ,  B ,  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1872   ifcif 3849   class class class wbr 4361   RRcr 9484    <_ cle 9622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-pre-lttri 9559
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator