ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqord1 Unicode version

Theorem eqord1 8268
Description: A strictly increasing real function on a subset of  RR is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by Jim Kingdon, 20-Dec-2022.)
Hypotheses
Ref Expression
ltord.1  |-  ( x  =  y  ->  A  =  B )
ltord.2  |-  ( x  =  C  ->  A  =  M )
ltord.3  |-  ( x  =  D  ->  A  =  N )
ltord.4  |-  S  C_  RR
ltord.5  |-  ( (
ph  /\  x  e.  S )  ->  A  e.  RR )
ltord.6  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  <  y  ->  A  <  B ) )
Assertion
Ref Expression
eqord1  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( C  =  D  <-> 
M  =  N ) )
Distinct variable groups:    x, B    x, y, C    x, D, y   
x, M, y    x, N, y    ph, x, y   
x, S, y
Allowed substitution hints:    A( x, y)    B( y)

Proof of Theorem eqord1
StepHypRef Expression
1 simprl 521 . . . . . 6  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  C  e.  S )
2 elisset 2703 . . . . . 6  |-  ( C  e.  S  ->  E. x  x  =  C )
31, 2syl 14 . . . . 5  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  E. x  x  =  C )
43adantr 274 . . . 4  |-  ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S )
)  /\  C  =  D )  ->  E. x  x  =  C )
5 ltord.2 . . . . . 6  |-  ( x  =  C  ->  A  =  M )
65adantl 275 . . . . 5  |-  ( ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S
) )  /\  C  =  D )  /\  x  =  C )  ->  A  =  M )
7 eqeq2 2150 . . . . . . . 8  |-  ( C  =  D  ->  (
x  =  C  <->  x  =  D ) )
87adantl 275 . . . . . . 7  |-  ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S )
)  /\  C  =  D )  ->  (
x  =  C  <->  x  =  D ) )
98biimpa 294 . . . . . 6  |-  ( ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S
) )  /\  C  =  D )  /\  x  =  C )  ->  x  =  D )
10 ltord.3 . . . . . 6  |-  ( x  =  D  ->  A  =  N )
119, 10syl 14 . . . . 5  |-  ( ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S
) )  /\  C  =  D )  /\  x  =  C )  ->  A  =  N )
126, 11eqtr3d 2175 . . . 4  |-  ( ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S
) )  /\  C  =  D )  /\  x  =  C )  ->  M  =  N )
134, 12exlimddv 1871 . . 3  |-  ( ( ( ph  /\  ( C  e.  S  /\  D  e.  S )
)  /\  C  =  D )  ->  M  =  N )
1413ex 114 . 2  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( C  =  D  ->  M  =  N ) )
15 ltord.1 . . . . . 6  |-  ( x  =  y  ->  A  =  B )
16 ltord.4 . . . . . 6  |-  S  C_  RR
17 ltord.5 . . . . . 6  |-  ( (
ph  /\  x  e.  S )  ->  A  e.  RR )
18 ltord.6 . . . . . 6  |-  ( (
ph  /\  ( x  e.  S  /\  y  e.  S ) )  -> 
( x  <  y  ->  A  <  B ) )
1915, 5, 10, 16, 17, 18ltordlem 8267 . . . . 5  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( C  <  D  ->  M  <  N ) )
2019con3d 621 . . . 4  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( -.  M  < 
N  ->  -.  C  <  D ) )
2115, 10, 5, 16, 17, 18ltordlem 8267 . . . . . 6  |-  ( (
ph  /\  ( D  e.  S  /\  C  e.  S ) )  -> 
( D  <  C  ->  N  <  M ) )
2221con3d 621 . . . . 5  |-  ( (
ph  /\  ( D  e.  S  /\  C  e.  S ) )  -> 
( -.  N  < 
M  ->  -.  D  <  C ) )
2322ancom2s 556 . . . 4  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( -.  N  < 
M  ->  -.  D  <  C ) )
2420, 23anim12d 333 . . 3  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( ( -.  M  <  N  /\  -.  N  <  M )  ->  ( -.  C  <  D  /\  -.  D  <  C ) ) )
2517ralrimiva 2508 . . . . . 6  |-  ( ph  ->  A. x  e.  S  A  e.  RR )
265eleq1d 2209 . . . . . . 7  |-  ( x  =  C  ->  ( A  e.  RR  <->  M  e.  RR ) )
2726rspccva 2791 . . . . . 6  |-  ( ( A. x  e.  S  A  e.  RR  /\  C  e.  S )  ->  M  e.  RR )
2825, 27sylan 281 . . . . 5  |-  ( (
ph  /\  C  e.  S )  ->  M  e.  RR )
2928adantrr 471 . . . 4  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  M  e.  RR )
3010eleq1d 2209 . . . . . . 7  |-  ( x  =  D  ->  ( A  e.  RR  <->  N  e.  RR ) )
3130rspccva 2791 . . . . . 6  |-  ( ( A. x  e.  S  A  e.  RR  /\  D  e.  S )  ->  N  e.  RR )
3225, 31sylan 281 . . . . 5  |-  ( (
ph  /\  D  e.  S )  ->  N  e.  RR )
3332adantrl 470 . . . 4  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  N  e.  RR )
3429, 33lttri3d 7901 . . 3  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( M  =  N  <-> 
( -.  M  < 
N  /\  -.  N  <  M ) ) )
3516, 1sseldi 3099 . . . 4  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  C  e.  RR )
36 simprr 522 . . . . 5  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  D  e.  S )
3716, 36sseldi 3099 . . . 4  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  ->  D  e.  RR )
3835, 37lttri3d 7901 . . 3  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( C  =  D  <-> 
( -.  C  < 
D  /\  -.  D  <  C ) ) )
3924, 34, 383imtr4d 202 . 2  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( M  =  N  ->  C  =  D ) )
4014, 39impbid 128 1  |-  ( (
ph  /\  ( C  e.  S  /\  D  e.  S ) )  -> 
( C  =  D  <-> 
M  =  N ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1332   E.wex 1469    e. wcel 1481   A.wral 2417    C_ wss 3075   class class class wbr 3936   RRcr 7642    < clt 7823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-cnex 7734  ax-resscn 7735  ax-pre-ltirr 7755  ax-pre-apti 7758
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-opab 3997  df-xp 4552  df-pnf 7825  df-mnf 7826  df-ltxr 7828
This theorem is referenced by:  eqord2  8269  reef11  11440
  Copyright terms: Public domain W3C validator