Theorem pssn2lp

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	⊢ ¬ ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfpss3	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) )
2	1	simprbi	⊢ ( 𝐴 ⊊ 𝐵 → ¬ 𝐵 ⊆ 𝐴 )
3		pssss	⊢ ( 𝐵 ⊊ 𝐴 → 𝐵 ⊆ 𝐴 )
4	2 3	nsyl	⊢ ( 𝐴 ⊊ 𝐵 → ¬ 𝐵 ⊊ 𝐴 )
5		imnan	⊢ ( ( 𝐴 ⊊ 𝐵 → ¬ 𝐵 ⊊ 𝐴 ) ↔ ¬ ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐴 ) )
6	4 5	mpbi	⊢ ¬ ( 𝐴 ⊊ 𝐵 ∧ 𝐵 ⊊ 𝐴 )