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

Theorem wetriext 4347
Description: A trichotomous well-order is extensional. (Contributed by Jim Kingdon, 26-Sep-2021.)
Hypotheses
Ref Expression
wetriext.we  |-  ( ph  ->  R  We  A )
wetriext.a  |-  ( ph  ->  A  e.  V )
wetriext.tri  |-  ( ph  ->  A. a  e.  A  A. b  e.  A  ( a R b  \/  a  =  b  \/  b R a ) )
wetriext.b  |-  ( ph  ->  B  e.  A )
wetriext.c  |-  ( ph  ->  C  e.  A )
wetriext.ext  |-  ( ph  ->  A. z  e.  A  ( z R B  <-> 
z R C ) )
Assertion
Ref Expression
wetriext  |-  ( ph  ->  B  =  C )
Distinct variable groups:    A, a, b   
z, A    B, a,
b    z, B    C, b    z, C    R, a, b    z, R
Allowed substitution hints:    ph( z, a, b)    C( a)    V( z, a, b)

Proof of Theorem wetriext
StepHypRef Expression
1 wetriext.b . . . . 5  |-  ( ph  ->  B  e.  A )
2 wetriext.ext . . . . 5  |-  ( ph  ->  A. z  e.  A  ( z R B  <-> 
z R C ) )
3 breq1 3808 . . . . . . 7  |-  ( z  =  B  ->  (
z R B  <->  B R B ) )
4 breq1 3808 . . . . . . 7  |-  ( z  =  B  ->  (
z R C  <->  B R C ) )
53, 4bibi12d 233 . . . . . 6  |-  ( z  =  B  ->  (
( z R B  <-> 
z R C )  <-> 
( B R B  <-> 
B R C ) ) )
65rspcv 2706 . . . . 5  |-  ( B  e.  A  ->  ( A. z  e.  A  ( z R B  <-> 
z R C )  ->  ( B R B  <->  B R C ) ) )
71, 2, 6sylc 61 . . . 4  |-  ( ph  ->  ( B R B  <-> 
B R C ) )
87biimpar 291 . . 3  |-  ( (
ph  /\  B R C )  ->  B R B )
9 wetriext.we . . . . . 6  |-  ( ph  ->  R  We  A )
10 wefr 4141 . . . . . 6  |-  ( R  We  A  ->  R  Fr  A )
119, 10syl 14 . . . . 5  |-  ( ph  ->  R  Fr  A )
12 wetriext.a . . . . 5  |-  ( ph  ->  A  e.  V )
13 frirrg 4133 . . . . 5  |-  ( ( R  Fr  A  /\  A  e.  V  /\  B  e.  A )  ->  -.  B R B )
1411, 12, 1, 13syl3anc 1170 . . . 4  |-  ( ph  ->  -.  B R B )
1514adantr 270 . . 3  |-  ( (
ph  /\  B R C )  ->  -.  B R B )
168, 15pm2.21dd 583 . 2  |-  ( (
ph  /\  B R C )  ->  B  =  C )
17 simpr 108 . 2  |-  ( (
ph  /\  B  =  C )  ->  B  =  C )
18 wetriext.c . . . . 5  |-  ( ph  ->  C  e.  A )
19 breq1 3808 . . . . . . 7  |-  ( z  =  C  ->  (
z R B  <->  C R B ) )
20 breq1 3808 . . . . . . 7  |-  ( z  =  C  ->  (
z R C  <->  C R C ) )
2119, 20bibi12d 233 . . . . . 6  |-  ( z  =  C  ->  (
( z R B  <-> 
z R C )  <-> 
( C R B  <-> 
C R C ) ) )
2221rspcv 2706 . . . . 5  |-  ( C  e.  A  ->  ( A. z  e.  A  ( z R B  <-> 
z R C )  ->  ( C R B  <->  C R C ) ) )
2318, 2, 22sylc 61 . . . 4  |-  ( ph  ->  ( C R B  <-> 
C R C ) )
2423biimpa 290 . . 3  |-  ( (
ph  /\  C R B )  ->  C R C )
25 frirrg 4133 . . . . 5  |-  ( ( R  Fr  A  /\  A  e.  V  /\  C  e.  A )  ->  -.  C R C )
2611, 12, 18, 25syl3anc 1170 . . . 4  |-  ( ph  ->  -.  C R C )
2726adantr 270 . . 3  |-  ( (
ph  /\  C R B )  ->  -.  C R C )
2824, 27pm2.21dd 583 . 2  |-  ( (
ph  /\  C R B )  ->  B  =  C )
29 wetriext.tri . . 3  |-  ( ph  ->  A. a  e.  A  A. b  e.  A  ( a R b  \/  a  =  b  \/  b R a ) )
30 breq1 3808 . . . . . 6  |-  ( a  =  B  ->  (
a R b  <->  B R
b ) )
31 eqeq1 2089 . . . . . 6  |-  ( a  =  B  ->  (
a  =  b  <->  B  =  b ) )
32 breq2 3809 . . . . . 6  |-  ( a  =  B  ->  (
b R a  <->  b R B ) )
3330, 31, 323orbi123d 1243 . . . . 5  |-  ( a  =  B  ->  (
( a R b  \/  a  =  b  \/  b R a )  <->  ( B R b  \/  B  =  b  \/  b R B ) ) )
34 breq2 3809 . . . . . 6  |-  ( b  =  C  ->  ( B R b  <->  B R C ) )
35 eqeq2 2092 . . . . . 6  |-  ( b  =  C  ->  ( B  =  b  <->  B  =  C ) )
36 breq1 3808 . . . . . 6  |-  ( b  =  C  ->  (
b R B  <->  C R B ) )
3734, 35, 363orbi123d 1243 . . . . 5  |-  ( b  =  C  ->  (
( B R b  \/  B  =  b  \/  b R B )  <->  ( B R C  \/  B  =  C  \/  C R B ) ) )
3833, 37rspc2v 2721 . . . 4  |-  ( ( B  e.  A  /\  C  e.  A )  ->  ( A. a  e.  A  A. b  e.  A  ( a R b  \/  a  =  b  \/  b R a )  ->  ( B R C  \/  B  =  C  \/  C R B ) ) )
391, 18, 38syl2anc 403 . . 3  |-  ( ph  ->  ( A. a  e.  A  A. b  e.  A  ( a R b  \/  a  =  b  \/  b R a )  ->  ( B R C  \/  B  =  C  \/  C R B ) ) )
4029, 39mpd 13 . 2  |-  ( ph  ->  ( B R C  \/  B  =  C  \/  C R B ) )
4116, 17, 28, 40mpjao3dan 1239 1  |-  ( ph  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103    \/ w3o 919    = wceq 1285    e. wcel 1434   A.wral 2353   class class class wbr 3805    Fr wfr 4111    We wwe 4113
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-v 2612  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-sn 3422  df-pr 3423  df-op 3425  df-br 3806  df-frfor 4114  df-frind 4115  df-wetr 4117
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator