Theorem sltssepcd 27943

Description: Two elements of separated sets obey less-than. Deduction form of sltssepc 27942. (Contributed by Scott Fenton, 25-Sep-2024.)

Hypotheses

Ref	Expression
sltssepcd.1	⊢ (𝜑 → 𝐴 <<s 𝐵)
sltssepcd.2	⊢ (𝜑 → 𝑋 ∈ 𝐴)
sltssepcd.3	⊢ (𝜑 → 𝑌 ∈ 𝐵)

Assertion

Ref	Expression
sltssepcd	⊢ (𝜑 → 𝑋 <s 𝑌)

Proof of Theorem sltssepcd

Step	Hyp	Ref	Expression
1		sltssepcd.1	. 2 ⊢ (𝜑 → 𝐴 <<s 𝐵)
2		sltssepcd.2	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
3		sltssepcd.3	. 2 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4		sltssepc 27942	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → 𝑋 <s 𝑌)

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5110   <s clts 27783   <<s cslts 27928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-slts 27929

This theorem is referenced by:  sltstr  27958  eqcuts3  27975  cofslts  28089  coinitslts  28090  cofcutrtime  28098  addsproplem2  28141  addsproplem4  28143  addsproplem5  28144  addsproplem6  28145  addsuniflem  28172  negsproplem2  28200  negsproplem4  28202  negsproplem5  28203  negsproplem6  28204  negsunif  28226  mulsproplem5  28291  mulsproplem6  28292  mulsproplem7  28293  mulsproplem8  28294  mulsproplem12  28298  sltmuls1  28318  sltmuls2  28319  mulsuniflem  28320  precsexlem11  28388  twocut  28594  pw2cut2  28633  bdayfinbndlem1  28638