Theorem tospos 18512

Description: A Toset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018.)

Assertion

Ref	Expression
tospos	⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset)

Proof of Theorem tospos

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2762	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
2		eqid 2762	. . 3 ⊢ (le‘𝐹) = (le‘𝐹)
3	1, 2	istos 18510	. 2 ⊢ (𝐹 ∈ Toset ↔ (𝐹 ∈ Poset ∧ ∀𝑥 ∈ (Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑦 ∨ 𝑦(le‘𝐹)𝑥)))
4	3	simplbi 502	1 ⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   ∈ wcel 2145  ∀wral 3078   class class class wbr 5107  ‘cfv 6537  Basecbs 17307  lecple 17355  Posetcpo 18401  Tosetctos 18508

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-toset 18509

This theorem is used by:  tltnle  18514  resstos  18524  omndadd2d  20263  omndadd2rd  20264  omndmul2  20266  omndmul  20268  gsumle  20278  orngsqr  21038  ofldchr  21795  odutos  33416  tlt3  33418  xrsclat  33459  isarchi3  33635  archirngz  33637  archiabllem1a  33639  archiabllem2c  33643  ordtrest2NEWlem  34440  ordtrest2NEW  34441  ordtconnlem1  34442  toslat  49916