Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  swoer Structured version   GIF 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 𝑅 = ((𝑋 × 𝑋) ∖ ( < < ))
swoer.2 ((φ (y 𝑋 z 𝑋)) → (y < z → ¬ z < y))
swoer.3 ((φ (x 𝑋 y 𝑋 z 𝑋)) → (x < y → (x < z z < y)))
Assertion
Ref Expression
swoer (φ𝑅 Er 𝑋)
Distinct variable groups:   x,y,z, <   φ,x,y,z   x,𝑋,y,z
Allowed substitution hints:   𝑅(x,y,z)

Proof of Theorem swoer
Dummy variables v u w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 swoer.1 . . . . 5 𝑅 = ((𝑋 × 𝑋) ∖ ( < < ))
2 difss 3064 . . . . 5 ((𝑋 × 𝑋) ∖ ( < < )) ⊆ (𝑋 × 𝑋)
31, 2eqsstri 2969 . . . 4 𝑅 ⊆ (𝑋 × 𝑋)
4 relxp 4390 . . . 4 Rel (𝑋 × 𝑋)
5 relss 4370 . . . 4 (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅))
63, 4, 5mp2 16 . . 3 Rel 𝑅
76a1i 9 . 2 (φ → Rel 𝑅)
8 simpr 103 . . 3 ((φ u𝑅v) → u𝑅v)
9 orcom 646 . . . . . 6 ((u < v v < u) ↔ (v < u u < v))
109a1i 9 . . . . 5 ((φ u𝑅v) → ((u < v v < u) ↔ (v < u u < v)))
1110notbid 591 . . . 4 ((φ u𝑅v) → (¬ (u < v v < u) ↔ ¬ (v < u u < v)))
123ssbri 3797 . . . . . . 7 (u𝑅vu(𝑋 × 𝑋)v)
1312adantl 262 . . . . . 6 ((φ u𝑅v) → u(𝑋 × 𝑋)v)
14 brxp 4318 . . . . . 6 (u(𝑋 × 𝑋)v ↔ (u 𝑋 v 𝑋))
1513, 14sylib 127 . . . . 5 ((φ u𝑅v) → (u 𝑋 v 𝑋))
161brdifun 6069 . . . . 5 ((u 𝑋 v 𝑋) → (u𝑅v ↔ ¬ (u < v v < u)))
1715, 16syl 14 . . . 4 ((φ u𝑅v) → (u𝑅v ↔ ¬ (u < v v < u)))
1815simprd 107 . . . . 5 ((φ u𝑅v) → v 𝑋)
1915simpld 105 . . . . 5 ((φ u𝑅v) → u 𝑋)
201brdifun 6069 . . . . 5 ((v 𝑋 u 𝑋) → (v𝑅u ↔ ¬ (v < u u < v)))
2118, 19, 20syl2anc 391 . . . 4 ((φ u𝑅v) → (v𝑅u ↔ ¬ (v < u u < v)))
2211, 17, 213bitr4d 209 . . 3 ((φ u𝑅v) → (u𝑅vv𝑅u))
238, 22mpbid 135 . 2 ((φ u𝑅v) → v𝑅u)
24 simprl 483 . . . . 5 ((φ (u𝑅v v𝑅w)) → u𝑅v)
2512ad2antrl 459 . . . . . . 7 ((φ (u𝑅v v𝑅w)) → u(𝑋 × 𝑋)v)
2614simplbi 259 . . . . . . 7 (u(𝑋 × 𝑋)vu 𝑋)
2725, 26syl 14 . . . . . 6 ((φ (u𝑅v v𝑅w)) → u 𝑋)
2814simprbi 260 . . . . . . 7 (u(𝑋 × 𝑋)vv 𝑋)
2925, 28syl 14 . . . . . 6 ((φ (u𝑅v v𝑅w)) → v 𝑋)
3027, 29, 16syl2anc 391 . . . . 5 ((φ (u𝑅v v𝑅w)) → (u𝑅v ↔ ¬ (u < v v < u)))
3124, 30mpbid 135 . . . 4 ((φ (u𝑅v v𝑅w)) → ¬ (u < v v < u))
32 simprr 484 . . . . 5 ((φ (u𝑅v v𝑅w)) → v𝑅w)
333brel 4335 . . . . . . . 8 (v𝑅w → (v 𝑋 w 𝑋))
3433simprd 107 . . . . . . 7 (v𝑅ww 𝑋)
3532, 34syl 14 . . . . . 6 ((φ (u𝑅v v𝑅w)) → w 𝑋)
361brdifun 6069 . . . . . 6 ((v 𝑋 w 𝑋) → (v𝑅w ↔ ¬ (v < w w < v)))
3729, 35, 36syl2anc 391 . . . . 5 ((φ (u𝑅v v𝑅w)) → (v𝑅w ↔ ¬ (v < w w < v)))
3832, 37mpbid 135 . . . 4 ((φ (u𝑅v v𝑅w)) → ¬ (v < w w < v))
39 simpl 102 . . . . . . 7 ((φ (u𝑅v v𝑅w)) → φ)
40 swoer.3 . . . . . . . 8 ((φ (x 𝑋 y 𝑋 z 𝑋)) → (x < y → (x < z z < y)))
4140swopolem 4033 . . . . . . 7 ((φ (u 𝑋 w 𝑋 v 𝑋)) → (u < w → (u < v v < w)))
4239, 27, 35, 29, 41syl13anc 1136 . . . . . 6 ((φ (u𝑅v v𝑅w)) → (u < w → (u < v v < w)))
4340swopolem 4033 . . . . . . . 8 ((φ (w 𝑋 u 𝑋 v 𝑋)) → (w < u → (w < v v < u)))
4439, 35, 27, 29, 43syl13anc 1136 . . . . . . 7 ((φ (u𝑅v v𝑅w)) → (w < u → (w < v v < u)))
45 orcom 646 . . . . . . 7 ((v < u w < v) ↔ (w < v v < u))
4644, 45syl6ibr 151 . . . . . 6 ((φ (u𝑅v v𝑅w)) → (w < u → (v < u w < v)))
4742, 46orim12d 699 . . . . 5 ((φ (u𝑅v v𝑅w)) → ((u < w w < u) → ((u < v v < w) (v < u w < v))))
48 or4 687 . . . . 5 (((u < v v < w) (v < u w < v)) ↔ ((u < v v < u) (v < w w < v)))
4947, 48syl6ib 150 . . . 4 ((φ (u𝑅v v𝑅w)) → ((u < w w < u) → ((u < v v < u) (v < w w < v))))
5031, 38, 49mtord 696 . . 3 ((φ (u𝑅v v𝑅w)) → ¬ (u < w w < u))
511brdifun 6069 . . . 4 ((u 𝑋 w 𝑋) → (u𝑅w ↔ ¬ (u < w w < u)))
5227, 35, 51syl2anc 391 . . 3 ((φ (u𝑅v v𝑅w)) → (u𝑅w ↔ ¬ (u < w w < u)))
5350, 52mpbird 156 . 2 ((φ (u𝑅v v𝑅w)) → u𝑅w)
54 swoer.2 . . . . . . 7 ((φ (y 𝑋 z 𝑋)) → (y < z → ¬ z < y))
5554, 40swopo 4034 . . . . . 6 (φ< Po 𝑋)
56 poirr 4035 . . . . . 6 (( < Po 𝑋 u 𝑋) → ¬ u < u)
5755, 56sylan 267 . . . . 5 ((φ u 𝑋) → ¬ u < u)
58 pm1.2 672 . . . . 5 ((u < u u < u) → u < u)
5957, 58nsyl 558 . . . 4 ((φ u 𝑋) → ¬ (u < u u < u))
60 simpr 103 . . . . 5 ((φ u 𝑋) → u 𝑋)
611brdifun 6069 . . . . 5 ((u 𝑋 u 𝑋) → (u𝑅u ↔ ¬ (u < u u < u)))
6260, 60, 61syl2anc 391 . . . 4 ((φ u 𝑋) → (u𝑅u ↔ ¬ (u < u u < u)))
6359, 62mpbird 156 . . 3 ((φ u 𝑋) → u𝑅u)
643ssbri 3797 . . . . 5 (u𝑅uu(𝑋 × 𝑋)u)
65 brxp 4318 . . . . . 6 (u(𝑋 × 𝑋)u ↔ (u 𝑋 u 𝑋))
6665simplbi 259 . . . . 5 (u(𝑋 × 𝑋)uu 𝑋)
6764, 66syl 14 . . . 4 (u𝑅uu 𝑋)
6867adantl 262 . . 3 ((φ u𝑅u) → u 𝑋)
6963, 68impbida 528 . 2 (φ → (u 𝑋u𝑅u))
707, 23, 53, 69iserd 6068 1 (φ𝑅 Er 𝑋)
 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   ∪ cun 2909   ⊆ wss 2911   class class class wbr 3755   Po wpo 4022   × 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-bnd 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