Theorem tospos 18341

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

Syntax hints:   → wi 4   ∨ wo 847   ∈ wcel 2113  ∀wral 3051   class class class wbr 5098  ‘cfv 6492  Basecbs 17136  lecple 17184  Posetcpo 18230  Tosetctos 18337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-toset 18338

This theorem is referenced by:  tltnle  18343  resstos  18353  omndadd2d  20059  omndadd2rd  20060  omndmul2  20062  omndmul  20064  gsumle  20074  orngsqr  20799  ofldchr  21531  odutos  33050  tlt3  33052  xrsclat  33093  isarchi3  33269  archirngz  33271  archiabllem1a  33273  archiabllem2c  33277  ordtrest2NEWlem  34079  ordtrest2NEW  34080  ordtconnlem1  34081  toslat  49223