Metamath Proof Explorer


Theorem f1od

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 )

Proof

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 )