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

Theorem posasymb 17264
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 1167 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Poset)
2 simp2 1168 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
3 simp3 1169 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
4 posi.b . . . . 5 𝐵 = (Base‘𝐾)
5 posi.l . . . . 5 = (le‘𝐾)
64, 5posi 17262 . . . 4 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑌𝐵)) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑌) → 𝑋 𝑌)))
71, 2, 3, 3, 6syl13anc 1492 . . 3 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑌) → 𝑋 𝑌)))
87simp2d 1174 . 2 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌))
94, 5posref 17263 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋 𝑋)
10 breq2 4845 . . . . 5 (𝑋 = 𝑌 → (𝑋 𝑋𝑋 𝑌))
119, 10syl5ibcom 237 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌𝑋 𝑌))
12 breq1 4844 . . . . 5 (𝑋 = 𝑌 → (𝑋 𝑋𝑌 𝑋))
139, 12syl5ibcom 237 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌𝑌 𝑋))
1411, 13jcad 509 . . 3 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌 → (𝑋 𝑌𝑌 𝑋)))
15143adant3 1163 . 2 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 = 𝑌 → (𝑋 𝑌𝑌 𝑋)))
168, 15impbid 204 1 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) ↔ 𝑋 = 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157   class class class wbr 4841  cfv 6099  Basecbs 16181  lecple 16271  Posetcpo 17252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-nul 4981
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-sbc 3632  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-br 4842  df-iota 6062  df-fv 6107  df-proset 17240  df-poset 17258
This theorem is referenced by:  pltnle  17278  pltval3  17279  lublecllem  17300  latasymb  17366  latleeqj1  17375  latleeqm1  17391  odupos  17447  poslubmo  17458  posglbmo  17459  posrasymb  30165  archirngz  30251  archiabllem1a  30253  ople0  35200  op1le  35205  atlle0  35318
  Copyright terms: Public domain W3C validator