MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssltsepcd Structured version   Visualization version   GIF version

Theorem ssltsepcd 27221
Description: Two elements of separated sets obey less-than. Deduction form of ssltsepc 27220. (Contributed by Scott Fenton, 25-Sep-2024.)
Hypotheses
Ref Expression
ssltsepcd.1 (𝜑𝐴 <<s 𝐵)
ssltsepcd.2 (𝜑𝑋𝐴)
ssltsepcd.3 (𝜑𝑌𝐵)
Assertion
Ref Expression
ssltsepcd (𝜑𝑋 <s 𝑌)

Proof of Theorem ssltsepcd
StepHypRef Expression
1 ssltsepcd.1 . 2 (𝜑𝐴 <<s 𝐵)
2 ssltsepcd.2 . 2 (𝜑𝑋𝐴)
3 ssltsepcd.3 . 2 (𝜑𝑌𝐵)
4 ssltsepc 27220 . 2 ((𝐴 <<s 𝐵𝑋𝐴𝑌𝐵) → 𝑋 <s 𝑌)
51, 2, 3, 4syl3anc 1371 1 (𝜑𝑋 <s 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106   class class class wbr 5141   <s cslt 27071   <<s csslt 27208
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-xp 5675  df-sslt 27209
This theorem is referenced by:  sslttr  27234  cofsslt  27325  coinitsslt  27326  cofcutrtime  27334  addsproplem2  27370  addsproplem4  27372  addsproplem5  27373  addsproplem6  27374  addsuniflem  27400  negsproplem2  27419  negsproplem4  27421  negsproplem5  27422  negsproplem6  27423  negsunif  27443  mulsproplem5  27489  mulsproplem6  27490  mulsproplem7  27491  mulsproplem8  27492  mulsproplem12  27496  ssltmul1  27514  ssltmul2  27515  mulsuniflem  27516
  Copyright terms: Public domain W3C validator