Theorem sdomirr

Description: Strict dominance is irreflexive. Theorem 21(i) of Suppes p. 97. (Contributed by NM, 4-Jun-1998)

	Ref	Expression
Assertion	sdomirr	$$⊢\neg A\prec A$$

Proof

Step	Hyp	Ref	Expression
1		sdomnen	$$⊢A\prec A\to \neg A\approx A$$
2		enrefg	$$⊢A\in \mathrm{V}\to A\approx A$$
3	1 2	nsyl3	$$⊢A\in \mathrm{V}\to \neg A\prec A$$
4		relsdom	$$⊢\mathrm{Rel}\prec$$
5	4	brrelex1i	$$⊢A\prec A\to A\in \mathrm{V}$$
6	5	con3i	$$⊢\neg A\in \mathrm{V}\to \neg A\prec A$$
7	3 6	pm2.61i	$$⊢\neg A\prec A$$