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

Syntax hints:   → wi 4   ∨ wo 843   ∈ wcel 2104  ∀wral 3059   class class class wbr 5149  ‘cfv 6544  Basecbs 17150  lecple 17210  Posetcpo 18266  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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-toset 18376

This theorem is referenced by:  tltnle  18381  resstos  32402  odutos  32403  tlt3  32405  xrsclat  32446  omndadd2d  32494  omndadd2rd  32495  omndmul2  32498  omndmul  32500  gsumle  32510  isarchi3  32601  archirngz  32603  archiabllem1a  32605  archiabllem2c  32609  orngsqr  32690  ofldchr  32700  ordtrest2NEWlem  33198  ordtrest2NEW  33199  ordtconnlem1  33200  toslat  47696