Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | f1od.1 | |- F = ( x e. A |-> C ) |
|
f1od.2 | |- ( ( ph /\ x e. A ) -> C e. W ) |
||
f1od.3 | |- ( ( ph /\ y e. B ) -> D e. X ) |
||
f1od.4 | |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) ) |
||
Assertion | f1od | |- ( ph -> F : A -1-1-onto-> B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1od.1 | |- F = ( x e. A |-> C ) |
|
2 | f1od.2 | |- ( ( ph /\ x e. A ) -> C e. W ) |
|
3 | f1od.3 | |- ( ( ph /\ y e. B ) -> D e. X ) |
|
4 | f1od.4 | |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) ) |
|
5 | 1 2 3 4 | f1ocnvd | |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) ) |
6 | 5 | simpld | |- ( ph -> F : A -1-1-onto-> B ) |