Theorem prsref

Description: "Less than or equal to" is reflexive in a proset. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	isprs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isprs.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	prsref	⊢ ( ( 𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		isprs.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		isprs.l	⊢ ≤ = ( le ‘ 𝐾 )
3		id	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐵 )
4	3 3 3	3jca	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
5	1 2	prslem	⊢ ( ( 𝐾 ∈ Proset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑋 ∧ 𝑋 ≤ 𝑋 ) → 𝑋 ≤ 𝑋 ) ) )
6	4 5	sylan2	⊢ ( ( 𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑋 ∧ 𝑋 ≤ 𝑋 ) → 𝑋 ≤ 𝑋 ) ) )
7	6	simpld	⊢ ( ( 𝐾 ∈ Proset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )