Theorem ssltsepcd 27705

Description: Two elements of separated sets obey less-than. Deduction form of ssltsepc 27704. (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

Step	Hyp	Ref	Expression
1		ssltsepcd.1	. 2 ⊢ (𝜑 → 𝐴 <<s 𝐵)
2		ssltsepcd.2	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
3		ssltsepcd.3	. 2 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
4		ssltsepc 27704	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → 𝑋 <s 𝑌)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092   <s cslt 27550   <<s csslt 27691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-sslt 27692

This theorem is referenced by:  sslttr  27718  eqscut3  27735  cofsslt  27831  coinitsslt  27832  cofcutrtime  27840  addsproplem2  27882  addsproplem4  27884  addsproplem5  27885  addsproplem6  27886  addsuniflem  27913  negsproplem2  27940  negsproplem4  27942  negsproplem5  27943  negsproplem6  27944  negsunif  27966  mulsproplem5  28028  mulsproplem6  28029  mulsproplem7  28030  mulsproplem8  28031  mulsproplem12  28035  ssltmul1  28055  ssltmul2  28056  mulsuniflem  28057  precsexlem11  28124  twocut  28315