Theorem posprs

Description: A poset is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Assertion	posprs	⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
3	1 2	ispos2	⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ Proset ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
4	3	simplbi	⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )