Theorem sltssepcd 28037

Description: Two elements of separated sets obey less-than. Deduction form of sltssepc 28036. (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 28036	. 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 27877   <<s cslts 28022

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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-slts 28023

This theorem is used by:  sltstr  28052  eqcuts3  28069  cofslts  28183  coinitslts  28184  cofcutrtime  28192  addsproplem2  28235  addsproplem4  28237  addsproplem5  28238  addsproplem6  28239  addsuniflem  28266  negsproplem2  28294  negsproplem4  28296  negsproplem5  28297  negsproplem6  28298  negsunif  28320  mulsproplem5  28385  mulsproplem6  28386  mulsproplem7  28387  mulsproplem8  28388  mulsproplem12  28392  sltmuls1  28412  sltmuls2  28413  mulsuniflem  28414  precsexlem11  28482  twocut  28688  pw2cut2  28727  bdayfinbndlem1  28732