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 syl5bb
 |-  ( 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 syl5eq
 |-  ( ( 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 syl5bb
 |-  ( ph -> ( Fun `' F <-> A. y E* x e. A y = B ) )