MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  posasymb Structured version   Visualization version   GIF version

Theorem posasymb 17160
Description: A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011.)
Hypotheses
Ref Expression
posi.b 𝐵 = (Base‘𝐾)
posi.l = (le‘𝐾)
Assertion
Ref Expression
posasymb ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) ↔ 𝑋 = 𝑌))

Proof of Theorem posasymb
StepHypRef Expression
1 simp1 1130 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Poset)
2 simp2 1131 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
3 simp3 1132 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
4 posi.b . . . . 5 𝐵 = (Base‘𝐾)
5 posi.l . . . . 5 = (le‘𝐾)
64, 5posi 17158 . . . 4 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑌𝐵)) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑌) → 𝑋 𝑌)))
71, 2, 3, 3, 6syl13anc 1478 . . 3 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑌) → 𝑋 𝑌)))
87simp2d 1137 . 2 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌))
94, 5posref 17159 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋 𝑋)
10 breq2 4791 . . . . 5 (𝑋 = 𝑌 → (𝑋 𝑋𝑋 𝑌))
119, 10syl5ibcom 235 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌𝑋 𝑌))
12 breq1 4790 . . . . 5 (𝑋 = 𝑌 → (𝑋 𝑋𝑌 𝑋))
139, 12syl5ibcom 235 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌𝑌 𝑋))
1411, 13jcad 502 . . 3 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌 → (𝑋 𝑌𝑌 𝑋)))
15143adant3 1126 . 2 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 = 𝑌 → (𝑋 𝑌𝑌 𝑋)))
168, 15impbid 202 1 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) ↔ 𝑋 = 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145   class class class wbr 4787  cfv 6030  Basecbs 16064  lecple 16156  Posetcpo 17148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-preset 17136  df-poset 17154
This theorem is referenced by:  pltnle  17174  pltval3  17175  lublecllem  17196  latasymb  17262  latleeqj1  17271  latleeqm1  17287  odupos  17343  poslubmo  17354  posglbmo  17355  posrasymb  29997  archirngz  30083  archiabllem1a  30085  ople0  34996  op1le  35001  atlle0  35114
  Copyright terms: Public domain W3C validator