Theorem soirri

Description: A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	soi.1	⊢ 𝑅 Or 𝑆
	soi.2	⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
Assertion	soirri	⊢ ¬ 𝐴 𝑅 𝐴

Proof

Step	Hyp	Ref	Expression
1		soi.1	⊢ 𝑅 Or 𝑆
2		soi.2	⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
3		sonr	⊢ ( ( 𝑅 Or 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ¬ 𝐴 𝑅 𝐴 )
4	1 3	mpan	⊢ ( 𝐴 ∈ 𝑆 → ¬ 𝐴 𝑅 𝐴 )
5	4	adantl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ¬ 𝐴 𝑅 𝐴 )
6	2	brel	⊢ ( 𝐴 𝑅 𝐴 → ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) )
7	6	con3i	⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ¬ 𝐴 𝑅 𝐴 )
8	5 7	pm2.61i	⊢ ¬ 𝐴 𝑅 𝐴