Theorem tospos 18379

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 2729	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
2		eqid 2729	. . 3 ⊢ (le‘𝐹) = (le‘𝐹)
3	1, 2	istos 18377	. 2 ⊢ (𝐹 ∈ Toset ↔ (𝐹 ∈ Poset ∧ ∀𝑥 ∈ (Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑦 ∨ 𝑦(le‘𝐹)𝑥)))
4	3	simplbi 497	1 ⊢ (𝐹 ∈ Toset → 𝐹 ∈ Poset)

Syntax hints:   → wi 4   ∨ wo 847   ∈ wcel 2109  ∀wral 3044   class class class wbr 5107  ‘cfv 6511  Basecbs 17179  lecple 17227  Posetcpo 18268  Tosetctos 18375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-toset 18376

This theorem is referenced by:  tltnle  18381  resstos  32893  odutos  32894  tlt3  32896  xrsclat  32949  omndadd2d  33022  omndadd2rd  33023  omndmul2  33026  omndmul  33028  gsumle  33038  isarchi3  33141  archirngz  33143  archiabllem1a  33145  archiabllem2c  33149  orngsqr  33282  ofldchr  33292  ordtrest2NEWlem  33912  ordtrest2NEW  33913  ordtconnlem1  33914  toslat  48970