Theorem tospos 18384

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

Syntax hints:   → wi 4   ∨ wo 848   ∈ wcel 2114  ∀wral 3051   class class class wbr 5085  ‘cfv 6498  Basecbs 17179  lecple 17227  Posetcpo 18273  Tosetctos 18380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-toset 18381

This theorem is referenced by:  tltnle  18386  resstos  18396  omndadd2d  20105  omndadd2rd  20106  omndmul2  20108  omndmul  20110  gsumle  20120  orngsqr  20843  ofldchr  21556  odutos  33028  tlt3  33030  xrsclat  33071  isarchi3  33248  archirngz  33250  archiabllem1a  33252  archiabllem2c  33256  ordtrest2NEWlem  34066  ordtrest2NEW  34067  ordtconnlem1  34068  toslat  49457