Theorem sltsdisj

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

	Ref	Expression
Assertion	sltsdisj	$$⊢A{\ll }_{s}B\to A\cap B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		sltsss1	$$⊢A{\ll }_{s}B\to A\subseteq \mathrm{No}$$
2	1	sselda	$$⊢\left(A{\ll }_{s}B\wedge x\in A\right)\to x\in \mathrm{No}$$
3		ltsirr	$$⊢x\in \mathrm{No}\to \neg x{<}_{s}x$$
4	2 3	syl	$$⊢\left(A{\ll }_{s}B\wedge x\in A\right)\to \neg x{<}_{s}x$$
5		sltssepc	$$⊢\left(A{\ll }_{s}B\wedge x\in A\wedge x\in B\right)\to x{<}_{s}x$$
6	5	3expa	$$⊢\left(\left(A{\ll }_{s}B\wedge x\in A\right)\wedge x\in B\right)\to x{<}_{s}x$$
7	4 6	mtand	$$⊢\left(A{\ll }_{s}B\wedge x\in A\right)\to \neg x\in B$$
8	7	ralrimiva	$$⊢A{\ll }_{s}B\to \forall x\in A\neg x\in B$$
9		disj	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\in A\neg x\in B$$
10	8 9	sylibr	$$⊢A{\ll }_{s}B\to A\cap B=\varnothing$$