Metamath Proof Explorer


Theorem enssdom

Description: Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998)

Ref Expression
Assertion enssdom

Proof

Step Hyp Ref Expression
1 relen Rel
2 f1of1 f : x 1-1 onto y f : x 1-1 y
3 2 eximi f f : x 1-1 onto y f f : x 1-1 y
4 opabidw x y x y | f f : x 1-1 onto y f f : x 1-1 onto y
5 opabidw x y x y | f f : x 1-1 y f f : x 1-1 y
6 3 4 5 3imtr4i x y x y | f f : x 1-1 onto y x y x y | f f : x 1-1 y
7 df-en = x y | f f : x 1-1 onto y
8 7 eleq2i x y x y x y | f f : x 1-1 onto y
9 df-dom = x y | f f : x 1-1 y
10 9 eleq2i x y x y x y | f f : x 1-1 y
11 6 8 10 3imtr4i x y x y
12 1 11 relssi