This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sdomirr

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

Ref Expression
Assertion sdomirr ⊢ ¬ A ≺ A

Proof

Step Hyp Ref Expression
1 sdomnen ⊢ A ≺ A → ¬ A ≈ A
2 enrefg ⊢ A ∈ V → A ≈ A
3 1 2 nsyl3 ⊢ A ∈ V → ¬ A ≺ A
4 relsdom ⊢ Rel ⁡ ≺
5 4 brrelex1i ⊢ A ≺ A → A ∈ V
6 5 con3i ⊢ ¬ A ∈ V → ¬ A ≺ A
7 3 6 pm2.61i ⊢ ¬ A ≺ A