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

Metamath Proof Explorer

Theorem 0nsr

Description: The empty set is not a signed real. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

Ref Expression
Assertion 0nsr ¬ ∅ ∈ R

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∅ = ∅
2 enrer ⊢ ~R Er ( P × P )
3 erdm ⊢ ( ~R Er ( P × P ) → dom ~R = ( P × P ) )
4 2 3 ax-mp ⊢ dom ~R = ( P × P )
5 elqsn0 ⊢ ( ( dom ~R = ( P × P ) ∧ ∅ ∈ ( ( P × P ) / ~R ) ) → ∅ ≠ ∅ )
6 4 5 mpan ⊢ ( ∅ ∈ ( ( P × P ) / ~R ) → ∅ ≠ ∅ )
7 df-nr ⊢ R = ( ( P × P ) / ~R )
8 6 7 eleq2s ⊢ ( ∅ ∈ R → ∅ ≠ ∅ )
9 8 necon2bi ⊢ ( ∅ = ∅ → ¬ ∅ ∈ R )
10 1 9 ax-mp ⊢ ¬ ∅ ∈ R