Metamath Proof Explorer

Theorem ssltdisj

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

Ref Expression
Assertion ssltdisj 
|- ( A < ( A i^i B ) = (/) )

Proof

Step Hyp Ref Expression
1 ssltss1 
 |-  ( A < A C_ No )
2 1 sselda 
 |-  ( ( A < x e. No )
3 sltirr 
 |-  ( x e. No -> -. x
4 2 3 syl 
 |-  ( ( A < -. x
5 ssltsepc 
 |-  ( ( A < x
6 5 3expa 
 |-  ( ( ( A < x
7 4 6 mtand 
 |-  ( ( A < -. x e. B )
8 7 ralrimiva 
 |-  ( A < A. x e. A -. x e. B )
9 disj 
 |-  ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )
10 8 9 sylibr 
 |-  ( A < ( A i^i B ) = (/) )