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

Metamath Proof Explorer

Theorem f1o3d

Description: Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 f1o3d.1 
 |-  ( ph -> F = ( x e. A |-> C ) )
2 f1o3d.2 
 |-  ( ( ph /\ x e. A ) -> C e. B )
3 f1o3d.3 
 |-  ( ( ph /\ y e. B ) -> D e. A )
4 f1o3d.4 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )
5 2 ralrimiva 
 |-  ( ph -> A. x e. A C e. B )
6 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
7 6 fnmpt 
 |-  ( A. x e. A C e. B -> ( x e. A |-> C ) Fn A )
8 5 7 syl 
 |-  ( ph -> ( x e. A |-> C ) Fn A )
9 1 fneq1d 
 |-  ( ph -> ( F Fn A <-> ( x e. A |-> C ) Fn A ) )
10 8 9 mpbird 
 |-  ( ph -> F Fn A )
11 3 ralrimiva 
 |-  ( ph -> A. y e. B D e. A )
12 eqid 
 |-  ( y e. B |-> D ) = ( y e. B |-> D )
13 12 fnmpt 
 |-  ( A. y e. B D e. A -> ( y e. B |-> D ) Fn B )
14 11 13 syl 
 |-  ( ph -> ( y e. B |-> D ) Fn B )
15 eleq1a 
 |-  ( C e. B -> ( y = C -> y e. B ) )
16 2 15 syl 
 |-  ( ( ph /\ x e. A ) -> ( y = C -> y e. B ) )
17 16 impr 
 |-  ( ( ph /\ ( x e. A /\ y = C ) ) -> y e. B )
18 4 biimpar 
 |-  ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ y = C ) -> x = D )
19 18 exp42 
 |-  ( ph -> ( x e. A -> ( y e. B -> ( y = C -> x = D ) ) ) )
20 19 com34 
 |-  ( ph -> ( x e. A -> ( y = C -> ( y e. B -> x = D ) ) ) )
21 20 imp32 
 |-  ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B -> x = D ) )
22 17 21 jcai 
 |-  ( ( ph /\ ( x e. A /\ y = C ) ) -> ( y e. B /\ x = D ) )
23 eleq1a 
 |-  ( D e. A -> ( x = D -> x e. A ) )
24 3 23 syl 
 |-  ( ( ph /\ y e. B ) -> ( x = D -> x e. A ) )
25 24 impr 
 |-  ( ( ph /\ ( y e. B /\ x = D ) ) -> x e. A )
26 4 biimpa 
 |-  ( ( ( ph /\ ( x e. A /\ y e. B ) ) /\ x = D ) -> y = C )
27 26 exp42 
 |-  ( ph -> ( x e. A -> ( y e. B -> ( x = D -> y = C ) ) ) )
28 27 com23 
 |-  ( ph -> ( y e. B -> ( x e. A -> ( x = D -> y = C ) ) ) )
29 28 com34 
 |-  ( ph -> ( y e. B -> ( x = D -> ( x e. A -> y = C ) ) ) )
30 29 imp32 
 |-  ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A -> y = C ) )
31 25 30 jcai 
 |-  ( ( ph /\ ( y e. B /\ x = D ) ) -> ( x e. A /\ y = C ) )
32 22 31 impbida 
 |-  ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )
33 32 opabbidv 
 |-  ( ph -> { <. y , x >. | ( x e. A /\ y = C ) } = { <. y , x >. | ( y e. B /\ x = D ) } )
34 df-mpt 
 |-  ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
35 1 34 eqtrdi 
 |-  ( ph -> F = { <. x , y >. | ( x e. A /\ y = C ) } )
36 35 cnveqd 
 |-  ( ph -> `' F = `' { <. x , y >. | ( x e. A /\ y = C ) } )
37 cnvopab 
 |-  `' { <. x , y >. | ( x e. A /\ y = C ) } = { <. y , x >. | ( x e. A /\ y = C ) }
38 36 37 eqtrdi 
 |-  ( ph -> `' F = { <. y , x >. | ( x e. A /\ y = C ) } )
39 df-mpt 
 |-  ( y e. B |-> D ) = { <. y , x >. | ( y e. B /\ x = D ) }
40 39 a1i 
 |-  ( ph -> ( y e. B |-> D ) = { <. y , x >. | ( y e. B /\ x = D ) } )
41 33 38 40 3eqtr4d 
 |-  ( ph -> `' F = ( y e. B |-> D ) )
42 41 fneq1d 
 |-  ( ph -> ( `' F Fn B <-> ( y e. B |-> D ) Fn B ) )
43 14 42 mpbird 
 |-  ( ph -> `' F Fn B )
44 dff1o4 
 |-  ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
45 10 43 44 sylanbrc 
 |-  ( ph -> F : A -1-1-onto-> B )
46 45 41 jca 
 |-  ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )