This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1ocnv2d

Description: Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses f1od.1 
|- F = ( x e. A |-> C )
f1o2d.2 
|- ( ( ph /\ x e. A ) -> C e. B )
f1o2d.3 
|- ( ( ph /\ y e. B ) -> D e. A )
f1o2d.4 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
Assertion f1ocnv2d 
|- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )

Proof

Step Hyp Ref Expression
1 f1od.1 
 |-  F = ( x e. A |-> C )
2 f1o2d.2 
 |-  ( ( ph /\ x e. A ) -> C e. B )
3 f1o2d.3 
 |-  ( ( ph /\ y e. B ) -> D e. A )
4 f1o2d.4 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
5 eleq1a 
 |-  ( C e. B -> ( y = C -> y e. B ) )
6 2 5 syl 
 |-  ( ( ph /\ x e. A ) -> ( y = C -> y e. B ) )
7 6 impr 
 |-  ( ( ph /\ ( x e. A /\ y = C ) ) -> y e. B )
8 4 biimpar 
 |-  ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ y = C ) -> x = D )
9 8 exp42 
 |-  ( ph -> ( x e. A -> ( y e. B -> ( y = C -> x = D ) ) ) )
10 9 com34 
 |-  ( ph -> ( x e. A -> ( y = C -> ( y e. B -> x = D ) ) ) )
11 10 imp32 
 |-  ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B -> x = D ) )
12 7 11 jcai 
 |-  ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B /\ x = D ) )
13 eleq1a 
 |-  ( D e. A -> ( x = D -> x e. A ) )
14 3 13 syl 
 |-  ( ( ph /\ y e. B ) -> ( x = D -> x e. A ) )
15 14 impr 
 |-  ( ( ph /\ ( y e. B /\ x = D ) ) -> x e. A )
16 4 biimpa 
 |-  ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ x = D ) -> y = C )
17 16 exp42 
 |-  ( ph -> ( x e. A -> ( y e. B -> ( x = D -> y = C ) ) ) )
18 17 com23 
 |-  ( ph -> ( y e. B -> ( x e. A -> ( x = D -> y = C ) ) ) )
19 18 com34 
 |-  ( ph -> ( y e. B -> ( x = D -> ( x e. A -> y = C ) ) ) )
20 19 imp32 
 |-  ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A -> y = C ) )
21 15 20 jcai 
 |-  ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A /\ y = C ) )
22 12 21 impbida 
 |-  ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )
23 1 2 3 22 f1ocnvd 
 |-  ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )