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

Theorem swoer 6070
Description: Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypotheses
Ref Expression
swoer.1  R  X  X.  X  \  .<  u.  `'  .<
swoer.2  X  X  .<  .<
swoer.3  X  X  X  .<  .<  .<
Assertion
Ref Expression
swoer  R  Er  X
Distinct variable groups:   ,,, 
.<   ,,,   , X,,
Allowed substitution hints:    R(,,)

Proof of Theorem swoer
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 swoer.1 . . . . 5  R  X  X.  X  \  .<  u.  `'  .<
2 difss 3064 . . . . 5  X  X.  X 
\  .<  u.  `'  .<  C_  X  X.  X
31, 2eqsstri 2969 . . . 4  R  C_  X  X.  X
4 relxp 4390 . . . 4  Rel  X  X.  X
5 relss 4370 . . . 4  R 
C_  X  X.  X  Rel  X  X.  X  Rel  R
63, 4, 5mp2 16 . . 3  Rel  R
76a1i 9 . 2  Rel  R
8 simpr 103 . . 3  R  R
9 orcom 646 . . . . . 6  .<  .< 
.<  .<
109a1i 9 . . . . 5  R  .<  .< 
.<  .<
1110notbid 591 . . . 4  R  .<  .<  .<  .<
123ssbri 3797 . . . . . . 7  R  X  X.  X
1312adantl 262 . . . . . 6  R  X  X.  X
14 brxp 4318 . . . . . 6  X  X.  X  X  X
1513, 14sylib 127 . . . . 5  R  X  X
161brdifun 6069 . . . . 5  X  X  R  .<  .<
1715, 16syl 14 . . . 4  R  R  .<  .<
1815simprd 107 . . . . 5  R  X
1915simpld 105 . . . . 5  R  X
201brdifun 6069 . . . . 5  X  X  R  .<  .<
2118, 19, 20syl2anc 391 . . . 4  R  R  .<  .<
2211, 17, 213bitr4d 209 . . 3  R  R  R
238, 22mpbid 135 . 2  R  R
24 simprl 483 . . . . 5  R  R  R
2512ad2antrl 459 . . . . . . 7  R  R  X  X.  X
2614simplbi 259 . . . . . . 7  X  X.  X  X
2725, 26syl 14 . . . . . 6  R  R  X
2814simprbi 260 . . . . . . 7  X  X.  X  X
2925, 28syl 14 . . . . . 6  R  R  X
3027, 29, 16syl2anc 391 . . . . 5  R  R  R  .<  .<
3124, 30mpbid 135 . . . 4  R  R  .<  .<
32 simprr 484 . . . . 5  R  R  R
333brel 4335 . . . . . . . 8  R  X  X
3433simprd 107 . . . . . . 7  R  X
3532, 34syl 14 . . . . . 6  R  R  X
361brdifun 6069 . . . . . 6  X  X  R  .<  .<
3729, 35, 36syl2anc 391 . . . . 5  R  R  R  .<  .<
3832, 37mpbid 135 . . . 4  R  R  .<  .<
39 simpl 102 . . . . . . 7  R  R
40 swoer.3 . . . . . . . 8  X  X  X  .<  .<  .<
4140swopolem 4033 . . . . . . 7  X  X  X  .<  .<  .<
4239, 27, 35, 29, 41syl13anc 1136 . . . . . 6  R  R  .<  .<  .<
4340swopolem 4033 . . . . . . . 8  X  X  X  .<  .<  .<
4439, 35, 27, 29, 43syl13anc 1136 . . . . . . 7  R  R  .<  .<  .<
45 orcom 646 . . . . . . 7  .<  .< 
.<  .<
4644, 45syl6ibr 151 . . . . . 6  R  R  .<  .<  .<
4742, 46orim12d 699 . . . . 5  R  R  .<  .<  .<  .<  .<  .<
48 or4 687 . . . . 5  .<  .<  .<  .<  .<  .<  .<  .<
4947, 48syl6ib 150 . . . 4  R  R  .<  .<  .<  .<  .<  .<
5031, 38, 49mtord 696 . . 3  R  R  .<  .<
511brdifun 6069 . . . 4  X  X  R  .<  .<
5227, 35, 51syl2anc 391 . . 3  R  R  R  .<  .<
5350, 52mpbird 156 . 2  R  R  R
54 swoer.2 . . . . . . 7  X  X  .<  .<
5554, 40swopo 4034 . . . . . 6  .<  Po  X
56 poirr 4035 . . . . . 6 
.<  Po  X  X  .<
5755, 56sylan 267 . . . . 5  X  .<
58 pm1.2 672 . . . . 5  .<  .<  .<
5957, 58nsyl 558 . . . 4  X 
.<  .<
60 simpr 103 . . . . 5  X  X
611brdifun 6069 . . . . 5  X  X  R  .<  .<
6260, 60, 61syl2anc 391 . . . 4  X  R 
.<  .<
6359, 62mpbird 156 . . 3  X  R
643ssbri 3797 . . . . 5  R  X  X.  X
65 brxp 4318 . . . . . 6  X  X.  X  X  X
6665simplbi 259 . . . . 5  X  X.  X  X
6764, 66syl 14 . . . 4  R  X
6867adantl 262 . . 3  R  X
6963, 68impbida 528 . 2  X  R
707, 23, 53, 69iserd 6068 1  R  Er  X
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 97   wb 98   wo 628   w3a 884   wceq 1242   wcel 1390    \ cdif 2908    u. cun 2909    C_ wss 2911   class class class wbr 3755    Po wpo 4022    X. cxp 4286   `'ccnv 4287   Rel wrel 4293    Er wer 6039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-po 4024  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-er 6042
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator