Metamath Proof Explorer


Theorem dfdom2

Description: Alternate definition of dominance. (Contributed by NM, 17-Jun-1998)

Ref Expression
Assertion dfdom2 ≼ = ( ≺ ∪ ≈ )

Proof

Step Hyp Ref Expression
1 df-sdom ≺ = ( ≼ ∖ ≈ )
2 1 uneq2i ( ≈ ∪ ≺ ) = ( ≈ ∪ ( ≼ ∖ ≈ ) )
3 uncom ( ≈ ∪ ≺ ) = ( ≺ ∪ ≈ )
4 enssdom ≈ ⊆ ≼
5 undif ( ≈ ⊆ ≼ ↔ ( ≈ ∪ ( ≼ ∖ ≈ ) ) = ≼ )
6 4 5 mpbi ( ≈ ∪ ( ≼ ∖ ≈ ) ) = ≼
7 2 3 6 3eqtr3ri ≼ = ( ≺ ∪ ≈ )