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 ¬ 𝐴 ≺ 𝐴

Proof

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