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

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 ) ) )