Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equinumerosity
enssdom
Next ⟩
dfdom2
Metamath Proof Explorer
Ascii
Unicode
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
⊢
≈
⊆
≼