Theorem tospos 18572

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 2761	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
2		eqid 2761	. . 3 ⊢ (le‘𝐹) = (le‘𝐹)
3	1, 2	istos 18570	. 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 3077   class class class wbr 5103  ‘cfv 6531  Basecbs 17367  lecple 17415  Posetcpo 18461  Tosetctos 18568

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 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-toset 18569

This theorem is used by:  tltnle  18574  resstos  18584  omndadd2d  20324  omndadd2rd  20325  omndmul2  20327  omndmul  20329  gsumle  20339  orngsqr  21103  ofldchr  21862  odutos  33511  tlt3  33513  xrsclat  33554  isarchi3  33730  archirngz  33732  archiabllem1a  33734  archiabllem2c  33738  ordtrest2NEWlem  34536  ordtrest2NEW  34537  ordtconnlem1  34538  toslat  50034