Metamath Proof Explorer

Theorem funcnvmpt

Description: Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017)

Ref Expression
Hypotheses funcnvmpt.0 
|- F/ x ph
funcnvmpt.1 
|- F/_ x A
funcnvmpt.2 
|- F/_ x F
funcnvmpt.3 
|- F = ( x e. A |-> B )
funcnvmpt.4 
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion funcnvmpt 
|- ( ph -> ( Fun `' F <-> A. y E* x e. A y = B ) )

Proof

Step Hyp Ref Expression
1 funcnvmpt.0 
 |-  F/ x ph
2 funcnvmpt.1 
 |-  F/_ x A
3 funcnvmpt.2 
 |-  F/_ x F
4 funcnvmpt.3 
 |-  F = ( x e. A |-> B )
5 funcnvmpt.4 
 |-  ( ( ph /\ x e. A ) -> B e. V )
6 relcnv 
 |-  Rel `' F
7 nfcv 
 |-  F/_ y `' F
8 3 nfcnv 
 |-  F/_ x `' F
9 7 8 dffun6f 
 |-  ( Fun `' F <-> ( Rel `' F /\ A. y E* x y `' F x ) )
10 6 9 mpbiran 
 |-  ( Fun `' F <-> A. y E* x y `' F x )
11 vex 
 |-  y e. _V
12 vex 
 |-  x e. _V
13 11 12 brcnv 
 |-  ( y `' F x <-> x F y )
14 13 mobii 
 |-  ( E* x y `' F x <-> E* x x F y )
15 14 albii 
 |-  ( A. y E* x y `' F x <-> A. y E* x x F y )
16 10 15 bitri 
 |-  ( Fun `' F <-> A. y E* x x F y )
17 4 funmpt2 
 |-  Fun F
18 funbrfv2b 
 |-  ( Fun F -> ( x F y <-> ( x e. dom F /\ ( F ` x ) = y ) ) )
19 17 18 ax-mp 
 |-  ( x F y <-> ( x e. dom F /\ ( F ` x ) = y ) )
20 4 dmmpt 
 |-  dom F = { x e. A | B e. _V }
21 5 elexd 
 |-  ( ( ph /\ x e. A ) -> B e. _V )
22 21 ex 
 |-  ( ph -> ( x e. A -> B e. _V ) )
23 1 22 ralrimi 
 |-  ( ph -> A. x e. A B e. _V )
24 2 rabid2f 
 |-  ( A = { x e. A | B e. _V } <-> A. x e. A B e. _V )
25 23 24 sylibr 
 |-  ( ph -> A = { x e. A | B e. _V } )
26 20 25 eqtr4id 
 |-  ( ph -> dom F = A )
27 26 eleq2d 
 |-  ( ph -> ( x e. dom F <-> x e. A ) )
28 27 anbi1d 
 |-  ( ph -> ( ( x e. dom F /\ ( F ` x ) = y ) <-> ( x e. A /\ ( F ` x ) = y ) ) )
29 19 28 bitrid 
 |-  ( ph -> ( x F y <-> ( x e. A /\ ( F ` x ) = y ) ) )
30 29 bian1d 
 |-  ( ph -> ( ( x e. A /\ x F y ) <-> ( x e. A /\ ( F ` x ) = y ) ) )
31 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
32 4 fveq1i 
 |-  ( F ` x ) = ( ( x e. A |-> B ) ` x )
33 2 fvmpt2f 
 |-  ( ( x e. A /\ B e. V ) -> ( ( x e. A |-> B ) ` x ) = B )
34 32 33 eqtrid 
 |-  ( ( x e. A /\ B e. V ) -> ( F ` x ) = B )
35 31 5 34 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
36 35 eqeq2d 
 |-  ( ( ph /\ x e. A ) -> ( y = ( F ` x ) <-> y = B ) )
37 eqcom 
 |-  ( ( F ` x ) = y <-> y = ( F ` x ) )
38 27 biimpar 
 |-  ( ( ph /\ x e. A ) -> x e. dom F )
39 funbrfvb 
 |-  ( ( Fun F /\ x e. dom F ) -> ( ( F ` x ) = y <-> x F y ) )
40 17 38 39 sylancr 
 |-  ( ( ph /\ x e. A ) -> ( ( F ` x ) = y <-> x F y ) )
41 37 40 bitr3id 
 |-  ( ( ph /\ x e. A ) -> ( y = ( F ` x ) <-> x F y ) )
42 36 41 bitr3d 
 |-  ( ( ph /\ x e. A ) -> ( y = B <-> x F y ) )
43 42 pm5.32da 
 |-  ( ph -> ( ( x e. A /\ y = B ) <-> ( x e. A /\ x F y ) ) )
44 30 43 29 3bitr4rd 
 |-  ( ph -> ( x F y <-> ( x e. A /\ y = B ) ) )
45 1 44 mobid 
 |-  ( ph -> ( E* x x F y <-> E* x ( x e. A /\ y = B ) ) )
46 df-rmo 
 |-  ( E* x e. A y = B <-> E* x ( x e. A /\ y = B ) )
47 45 46 bitr4di 
 |-  ( ph -> ( E* x x F y <-> E* x e. A y = B ) )
48 47 albidv 
 |-  ( ph -> ( A. y E* x x F y <-> A. y E* x e. A y = B ) )
49 16 48 bitrid 
 |-  ( ph -> ( Fun `' F <-> A. y E* x e. A y = B ) )