Theorem sltssepc

Description: Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	sltssepc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 <s 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		sltssep	⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
2		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 <s 𝑦 ↔ 𝑋 <s 𝑦 ) )
3		breq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 <s 𝑦 ↔ 𝑋 <s 𝑌 ) )
4	2 3	rspc2va	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) → 𝑋 <s 𝑌 )
5	4	ancoms	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 <s 𝑌 )
6	1 5	sylan	⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 <s 𝑌 )
7	6	3impb	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 <s 𝑌 )