ssltdisj

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

		Ref	Expression
	Assertion	ssltdisj	$⊢ A ≪_{s} B \to A \cap B = \emptyset$

Step	Hyp	Ref	Expression
1		ssltss1	$⊢ A ≪_{s} B \to A \subseteq No$
2	1	sselda	$⊢ (A ≪_{s} B \land x \in A) \to x \in No$
3		sltirr	$⊢ x \in No \to \neg x <_{s} x$
4	2 3	syl	$⊢ (A ≪_{s} B \land x \in A) \to \neg x <_{s} x$
5		ssltsepc	$⊢ (A ≪_{s} B \land x \in A \land x \in B) \to x <_{s} x$
6	5	3expa	$⊢ ((A ≪_{s} B \land x \in A) \land x \in B) \to x <_{s} x$
7	4 6	mtand	$⊢ (A ≪_{s} B \land x \in A) \to \neg x \in B$
8	7	ralrimiva	$⊢ A ≪_{s} B \to \forall x \in A \neg x \in B$
9		disj	$⊢ A \cap B = \emptyset \leftrightarrow \forall x \in A \neg x \in B$
10	8 9	sylibr	$⊢ A ≪_{s} B \to A \cap B = \emptyset$

Metamath Proof Explorer