Metamath Proof Explorer
Description: Two elements of separated sets obey less than. Deduction form of
ssltsepc . (Contributed by Scott Fenton, 25-Sep-2024)
|
|
Ref |
Expression |
|
Hypotheses |
ssltsepcd.1 |
|- ( ph -> A < |
|
|
ssltsepcd.2 |
|- ( ph -> X e. A ) |
|
|
ssltsepcd.3 |
|- ( ph -> Y e. B ) |
|
Assertion |
ssltsepcd |
|- ( ph -> X |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssltsepcd.1 |
|- ( ph -> A < |
| 2 |
|
ssltsepcd.2 |
|- ( ph -> X e. A ) |
| 3 |
|
ssltsepcd.3 |
|- ( ph -> Y e. B ) |
| 4 |
|
ssltsepc |
|- ( ( A < X |
| 5 |
1 2 3 4
|
syl3anc |
|- ( ph -> X |