Metamath Proof Explorer


Theorem funcnv4mpt

Description: Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-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 funcnv4mpt
|- ( ph -> ( Fun `' F <-> A. i e. A A. j e. A ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ 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 nfv
 |-  F/ i ph
7 nfcv
 |-  F/_ i A
8 nfcv
 |-  F/_ i F
9 nfcv
 |-  F/_ i B
10 nfcsb1v
 |-  F/_ x [_ i / x ]_ B
11 csbeq1a
 |-  ( x = i -> B = [_ i / x ]_ B )
12 2 7 9 10 11 cbvmptf
 |-  ( x e. A |-> B ) = ( i e. A |-> [_ i / x ]_ B )
13 4 12 eqtri
 |-  F = ( i e. A |-> [_ i / x ]_ B )
14 5 sbimi
 |-  ( [ i / x ] ( ph /\ x e. A ) -> [ i / x ] B e. V )
15 nfcv
 |-  F/_ x i
16 15 2 nfel
 |-  F/ x i e. A
17 1 16 nfan
 |-  F/ x ( ph /\ i e. A )
18 eleq1w
 |-  ( x = i -> ( x e. A <-> i e. A ) )
19 18 anbi2d
 |-  ( x = i -> ( ( ph /\ x e. A ) <-> ( ph /\ i e. A ) ) )
20 17 19 sbiev
 |-  ( [ i / x ] ( ph /\ x e. A ) <-> ( ph /\ i e. A ) )
21 nfcv
 |-  F/_ x V
22 10 21 nfel
 |-  F/ x [_ i / x ]_ B e. V
23 11 eleq1d
 |-  ( x = i -> ( B e. V <-> [_ i / x ]_ B e. V ) )
24 22 23 sbiev
 |-  ( [ i / x ] B e. V <-> [_ i / x ]_ B e. V )
25 14 20 24 3imtr3i
 |-  ( ( ph /\ i e. A ) -> [_ i / x ]_ B e. V )
26 csbeq1
 |-  ( i = j -> [_ i / x ]_ B = [_ j / x ]_ B )
27 6 7 8 13 25 26 funcnv5mpt
 |-  ( ph -> ( Fun `' F <-> A. i e. A A. j e. A ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ B ) ) )