Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tleile Structured version   Visualization version   GIF version

Theorem tleile 30659
Description: In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 11-Feb-2018.)
Hypotheses
Ref Expression
tleile.b 𝐵 = (Base‘𝐾)
tleile.l = (le‘𝐾)
Assertion
Ref Expression
tleile ((𝐾 ∈ Toset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 𝑋))

Proof of Theorem tleile
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1134 . 2 ((𝐾 ∈ Toset ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
2 simp3 1135 . 2 ((𝐾 ∈ Toset ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
3 tleile.b . . . . 5 𝐵 = (Base‘𝐾)
4 tleile.l . . . . 5 = (le‘𝐾)
53, 4istos 17645 . . . 4 (𝐾 ∈ Toset ↔ (𝐾 ∈ Poset ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 𝑥)))
65simprbi 500 . . 3 (𝐾 ∈ Toset → ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 𝑥))
763ad2ant1 1130 . 2 ((𝐾 ∈ Toset ∧ 𝑋𝐵𝑌𝐵) → ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 𝑥))
8 breq1 5055 . . . 4 (𝑥 = 𝑋 → (𝑥 𝑦𝑋 𝑦))
9 breq2 5056 . . . 4 (𝑥 = 𝑋 → (𝑦 𝑥𝑦 𝑋))
108, 9orbi12d 916 . . 3 (𝑥 = 𝑋 → ((𝑥 𝑦𝑦 𝑥) ↔ (𝑋 𝑦𝑦 𝑋)))
11 breq2 5056 . . . 4 (𝑦 = 𝑌 → (𝑋 𝑦𝑋 𝑌))
12 breq1 5055 . . . 4 (𝑦 = 𝑌 → (𝑦 𝑋𝑌 𝑋))
1311, 12orbi12d 916 . . 3 (𝑦 = 𝑌 → ((𝑋 𝑦𝑦 𝑋) ↔ (𝑋 𝑌𝑌 𝑋)))
1410, 13rspc2va 3620 . 2 (((𝑋𝐵𝑌𝐵) ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 𝑥)) → (𝑋 𝑌𝑌 𝑋))
151, 2, 7, 14syl21anc 836 1 ((𝐾 ∈ Toset ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 844  w3a 1084   = wceq 1538  wcel 2115  wral 3133   class class class wbr 5052  cfv 6343  Basecbs 16483  lecple 16572  Posetcpo 17550  Tosetctos 17643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-nul 5196
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-toset 17644
This theorem is referenced by:  tltnle  30660  odutos  30661  trleile  30664
  Copyright terms: Public domain W3C validator