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

Theorem swoer 7397
 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
swoer.2
swoer.3
Assertion
Ref Expression
swoer
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem swoer
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 swoer.1 . . . . 5
2 difss 3593 . . . . 5
31, 2eqsstri 3495 . . . 4
4 relxp 4959 . . . 4
5 relss 4939 . . . 4
63, 4, 5mp2 9 . . 3
76a1i 11 . 2
8 simpr 463 . . 3
9 orcom 389 . . . . . 6
109a1i 11 . . . . 5
1110notbid 296 . . . 4
123ssbri 4464 . . . . . . 7
1312adantl 468 . . . . . 6
14 brxp 4882 . . . . . 6
1513, 14sylib 200 . . . . 5
161brdifun 7396 . . . . 5
1715, 16syl 17 . . . 4
1815simprd 465 . . . . 5
1915simpld 461 . . . . 5
201brdifun 7396 . . . . 5
2118, 19, 20syl2anc 666 . . . 4
2211, 17, 213bitr4d 289 . . 3
238, 22mpbid 214 . 2
24 simprl 763 . . . . 5
2512ad2antrl 733 . . . . . . 7
2614simplbi 462 . . . . . . 7
2725, 26syl 17 . . . . . 6
2814simprbi 466 . . . . . . 7
2925, 28syl 17 . . . . . 6
3027, 29, 16syl2anc 666 . . . . 5
3124, 30mpbid 214 . . . 4
32 simprr 765 . . . . 5
333brel 4900 . . . . . . . 8
3433simprd 465 . . . . . . 7
3532, 34syl 17 . . . . . 6
361brdifun 7396 . . . . . 6
3729, 35, 36syl2anc 666 . . . . 5
3832, 37mpbid 214 . . . 4
39 simpl 459 . . . . . . 7
40 swoer.3 . . . . . . . 8
4140swopolem 4781 . . . . . . 7
4239, 27, 35, 29, 41syl13anc 1267 . . . . . 6
4340swopolem 4781 . . . . . . . 8
4439, 35, 27, 29, 43syl13anc 1267 . . . . . . 7
45 orcom 389 . . . . . . 7
4644, 45syl6ibr 231 . . . . . 6
4742, 46orim12d 847 . . . . 5
48 or4 531 . . . . 5
4947, 48syl6ib 230 . . . 4
5031, 38, 49mtord 665 . . 3
511brdifun 7396 . . . 4
5227, 35, 51syl2anc 666 . . 3
5350, 52mpbird 236 . 2
54 swoer.2 . . . . . . 7
5554, 40swopo 4782 . . . . . 6
56 poirr 4783 . . . . . 6
5755, 56sylan 474 . . . . 5
58 pm1.2 516 . . . . 5
5957, 58nsyl 125 . . . 4
60 simpr 463 . . . . 5
611brdifun 7396 . . . . 5
6260, 60, 61syl2anc 666 . . . 4
6359, 62mpbird 236 . . 3
643ssbri 4464 . . . . 5
65 brxp 4882 . . . . . 6
6665simplbi 462 . . . . 5
6764, 66syl 17 . . . 4
6867adantl 468 . . 3
6963, 68impbida 841 . 2
707, 23, 53, 69iserd 7395 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wo 370   wa 371   w3a 983   wceq 1438   wcel 1869   cdif 3434   cun 3435   wss 3437   class class class wbr 4421   wpo 4770   cxp 4849  ccnv 4850   wrel 4856   wer 7366 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-po 4772  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-er 7369 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator