Theorem sltssepcd 28140

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103   <s clts 27980   <<s cslts 28125

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-slts 28126

This theorem is used by:  sltstr  28155  eqcuts3  28172  cofslts  28286  coinitslts  28287  cofcutrtime  28295  addsproplem2  28338  addsproplem4  28340  addsproplem5  28341  addsproplem6  28342  addsuniflem  28369  negsproplem2  28397  negsproplem4  28399  negsproplem5  28400  negsproplem6  28401  negsunif  28423  mulsproplem5  28488  mulsproplem6  28489  mulsproplem7  28490  mulsproplem8  28491  mulsproplem12  28495  sltmuls1  28515  sltmuls2  28516  mulsuniflem  28517  precsexlem11  28585  twocut  28791  pw2cut2  28830  bdayfinbndlem1  28835