Theorem sltssepcd 28002

Description: Two elements of separated sets obey less-than. Deduction form of sltssepc 28001. (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 28001	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → 𝑋 <s 𝑌)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → 𝑋 <s 𝑌)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5114   <s clts 27842   <<s cslts 27987

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-slts 27988

This theorem is used by:  sltstr  28017  eqcuts3  28034  cofslts  28148  coinitslts  28149  cofcutrtime  28157  addsproplem2  28200  addsproplem4  28202  addsproplem5  28203  addsproplem6  28204  addsuniflem  28231  negsproplem2  28259  negsproplem4  28261  negsproplem5  28262  negsproplem6  28263  negsunif  28285  mulsproplem5  28350  mulsproplem6  28351  mulsproplem7  28352  mulsproplem8  28353  mulsproplem12  28357  sltmuls1  28377  sltmuls2  28378  mulsuniflem  28379  precsexlem11  28447  twocut  28653  pw2cut2  28692  bdayfinbndlem1  28697