Description: A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | fndmeng | |- ( ( F Fn A /\ A e. C ) -> A ~~ F ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnex | |- ( ( F Fn A /\ A e. C ) -> F e. _V ) |
|
2 | fnfun | |- ( F Fn A -> Fun F ) |
|
3 | 2 | adantr | |- ( ( F Fn A /\ A e. C ) -> Fun F ) |
4 | fundmeng | |- ( ( F e. _V /\ Fun F ) -> dom F ~~ F ) |
|
5 | 1 3 4 | syl2anc | |- ( ( F Fn A /\ A e. C ) -> dom F ~~ F ) |
6 | fndm | |- ( F Fn A -> dom F = A ) |
|
7 | 6 | breq1d | |- ( F Fn A -> ( dom F ~~ F <-> A ~~ F ) ) |
8 | 7 | adantr | |- ( ( F Fn A /\ A e. C ) -> ( dom F ~~ F <-> A ~~ F ) ) |
9 | 5 8 | mpbid | |- ( ( F Fn A /\ A e. C ) -> A ~~ F ) |