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

Theorem posasymb 17538
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 1132 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Poset)
2 simp2 1133 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
3 simp3 1134 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
4 posi.b . . . . 5 𝐵 = (Base‘𝐾)
5 posi.l . . . . 5 = (le‘𝐾)
64, 5posi 17536 . . . 4 ((𝐾 ∈ Poset ∧ (𝑋𝐵𝑌𝐵𝑌𝐵)) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑌) → 𝑋 𝑌)))
71, 2, 3, 3, 6syl13anc 1368 . . 3 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑋 ∧ ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌) ∧ ((𝑋 𝑌𝑌 𝑌) → 𝑋 𝑌)))
87simp2d 1139 . 2 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) → 𝑋 = 𝑌))
94, 5posref 17537 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋 𝑋)
10 breq2 5044 . . . . 5 (𝑋 = 𝑌 → (𝑋 𝑋𝑋 𝑌))
119, 10syl5ibcom 247 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌𝑋 𝑌))
12 breq1 5043 . . . . 5 (𝑋 = 𝑌 → (𝑋 𝑋𝑌 𝑋))
139, 12syl5ibcom 247 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌𝑌 𝑋))
1411, 13jcad 515 . . 3 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → (𝑋 = 𝑌 → (𝑋 𝑌𝑌 𝑋)))
15143adant3 1128 . 2 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 = 𝑌 → (𝑋 𝑌𝑌 𝑋)))
168, 15impbid 214 1 ((𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌𝑌 𝑋) ↔ 𝑋 = 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083   = wceq 1537  wcel 2114   class class class wbr 5040  cfv 6329  Basecbs 16459  lecple 16548  Posetcpo 17526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-nul 5184
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3752  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-nul 4268  df-if 4442  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4813  df-br 5041  df-iota 6288  df-fv 6337  df-proset 17514  df-poset 17532
This theorem is referenced by:  pltnle  17552  pltval3  17553  lublecllem  17574  latasymb  17640  latleeqj1  17649  latleeqm1  17665  odupos  17721  poslubmo  17732  posglbmo  17733  posrasymb  30628  archirngz  30823  archiabllem1a  30825  ople0  36356  op1le  36361  atlle0  36474
  Copyright terms: Public domain W3C validator