Theorem sltsdisj

Description: If A preceeds B , then A and B are disjoint. (Contributed by Scott Fenton, 18-Sep-2024)

	Ref	Expression
Assertion	sltsdisj	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 ∩ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		sltsss1	⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
2	1	sselda	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
3		ltsirr	⊢ ( 𝑥 ∈ No → ¬ 𝑥 <s 𝑥 )
4	2 3	syl	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 <s 𝑥 )
5		sltssepc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 <s 𝑥 )
6	5	3expa	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 <s 𝑥 )
7	4 6	mtand	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ 𝐵 )
8	7	ralrimiva	⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
9		disj	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
10	8 9	sylibr	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 ∩ 𝐵 ) = ∅ )