Description: Proper subclass has no 2-cycle loops. Compare Theorem 8 of Suppes p. 23. (Contributed by NM, 7-Feb-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pssn2lp | |- -. ( A C. B /\ B C. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfpss3 | |- ( A C. B <-> ( A C_ B /\ -. B C_ A ) ) |
|
| 2 | 1 | simprbi | |- ( A C. B -> -. B C_ A ) |
| 3 | pssss | |- ( B C. A -> B C_ A ) |
|
| 4 | 2 3 | nsyl | |- ( A C. B -> -. B C. A ) |
| 5 | imnan | |- ( ( A C. B -> -. B C. A ) <-> -. ( A C. B /\ B C. A ) ) |
|
| 6 | 4 5 | mpbi | |- -. ( A C. B /\ B C. A ) |