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