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

Metamath Proof Explorer

Theorem fmptdF

Description: Domain and codomain of the mapping operation; deduction form. This version of fmptd uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017)

Ref Expression
Hypotheses fmptdF.p 
|- F/ x ph
fmptdF.a 
|- F/_ x A
fmptdF.c 
|- F/_ x C
fmptdF.1 
|- ( ( ph /\ x e. A ) -> B e. C )
fmptdF.2 
|- F = ( x e. A |-> B )
Assertion fmptdF 
|- ( ph -> F : A --> C )

Proof

Step Hyp Ref Expression
1 fmptdF.p 
 |-  F/ x ph
2 fmptdF.a 
 |-  F/_ x A
3 fmptdF.c 
 |-  F/_ x C
4 fmptdF.1 
 |-  ( ( ph /\ x e. A ) -> B e. C )
5 fmptdF.2 
 |-  F = ( x e. A |-> B )
6 4 sbimi 
 |-  ( [ y / x ] ( ph /\ x e. A ) -> [ y / x ] B e. C )
7 sban 
 |-  ( [ y / x ] ( ph /\ x e. A ) <-> ( [ y / x ] ph /\ [ y / x ] x e. A ) )
8 1 sbf 
 |-  ( [ y / x ] ph <-> ph )
9 2 clelsb1fw 
 |-  ( [ y / x ] x e. A <-> y e. A )
10 8 9 anbi12i 
 |-  ( ( [ y / x ] ph /\ [ y / x ] x e. A ) <-> ( ph /\ y e. A ) )
11 7 10 bitri 
 |-  ( [ y / x ] ( ph /\ x e. A ) <-> ( ph /\ y e. A ) )
12 sbsbc 
 |-  ( [ y / x ] B e. C <-> [. y / x ]. B e. C )
13 sbcel12 
 |-  ( [. y / x ]. B e. C <-> [_ y / x ]_ B e. [_ y / x ]_ C )
14 vex 
 |-  y e. _V
15 14 3 csbgfi 
 |-  [_ y / x ]_ C = C
16 15 eleq2i 
 |-  ( [_ y / x ]_ B e. [_ y / x ]_ C <-> [_ y / x ]_ B e. C )
17 13 16 bitri 
 |-  ( [. y / x ]. B e. C <-> [_ y / x ]_ B e. C )
18 12 17 bitri 
 |-  ( [ y / x ] B e. C <-> [_ y / x ]_ B e. C )
19 6 11 18 3imtr3i 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. C )
20 19 ralrimiva 
 |-  ( ph -> A. y e. A [_ y / x ]_ B e. C )
21 nfcv 
 |-  F/_ y A
22 nfcv 
 |-  F/_ y B
23 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
24 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
25 2 21 22 23 24 cbvmptf 
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
26 25 fmpt 
 |-  ( A. y e. A [_ y / x ]_ B e. C <-> ( x e. A |-> B ) : A --> C )
27 20 26 sylib 
 |-  ( ph -> ( x e. A |-> B ) : A --> C )
28 5 feq1i 
 |-  ( F : A --> C <-> ( x e. A |-> B ) : A --> C )
29 27 28 sylibr 
 |-  ( ph -> F : A --> C )