Metamath Proof Explorer

Theorem tayl0

Description: The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses taylfval.s 
|- ( ph -> S e. { RR , CC } )
taylfval.f 
|- ( ph -> F : A --> CC )
taylfval.a 
|- ( ph -> A C_ S )
taylfval.n 
|- ( ph -> ( N e. NN0 \/ N = +oo ) )
taylfval.b 
|- ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
taylfval.t 
|- T = ( N ( S Tayl F ) B )
Assertion tayl0 
|- ( ph -> ( B e. dom T /\ ( T ` B ) = ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 taylfval.s 
 |-  ( ph -> S e. { RR , CC } )
2 taylfval.f 
 |-  ( ph -> F : A --> CC )
3 taylfval.a 
 |-  ( ph -> A C_ S )
4 taylfval.n 
 |-  ( ph -> ( N e. NN0 \/ N = +oo ) )
5 taylfval.b 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> B e. dom ( ( S Dn F ) ` k ) )
6 taylfval.t 
 |-  T = ( N ( S Tayl F ) B )
7 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
8 1 7 syl 
 |-  ( ph -> S C_ CC )
9 3 8 sstrd 
 |-  ( ph -> A C_ CC )
10 fveq2 
 |-  ( k = 0 -> ( ( S Dn F ) ` k ) = ( ( S Dn F ) ` 0 ) )
11 10 dmeqd 
 |-  ( k = 0 -> dom ( ( S Dn F ) ` k ) = dom ( ( S Dn F ) ` 0 ) )
12 11 eleq2d 
 |-  ( k = 0 -> ( B e. dom ( ( S Dn F ) ` k ) <-> B e. dom ( ( S Dn F ) ` 0 ) ) )
13 5 ralrimiva 
 |-  ( ph -> A. k e. ( ( 0 [,] N ) i^i ZZ ) B e. dom ( ( S Dn F ) ` k ) )
14 elxnn0 
 |-  ( N e. NN0* <-> ( N e. NN0 \/ N = +oo ) )
15 0xr 
 |-  0 e. RR*
16 15 a1i 
 |-  ( N e. NN0* -> 0 e. RR* )
17 xnn0xr 
 |-  ( N e. NN0* -> N e. RR* )
18 xnn0ge0 
 |-  ( N e. NN0* -> 0 <_ N )
19 lbicc2 
 |-  ( ( 0 e. RR* /\ N e. RR* /\ 0 <_ N ) -> 0 e. ( 0 [,] N ) )
20 16 17 18 19 syl3anc 
 |-  ( N e. NN0* -> 0 e. ( 0 [,] N ) )
21 14 20 sylbir 
 |-  ( ( N e. NN0 \/ N = +oo ) -> 0 e. ( 0 [,] N ) )
22 4 21 syl 
 |-  ( ph -> 0 e. ( 0 [,] N ) )
23 0zd 
 |-  ( ph -> 0 e. ZZ )
24 22 23 elind 
 |-  ( ph -> 0 e. ( ( 0 [,] N ) i^i ZZ ) )
25 12 13 24 rspcdva 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` 0 ) )
26 cnex 
 |-  CC e. _V
27 26 a1i 
 |-  ( ph -> CC e. _V )
28 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
29 27 1 2 3 28 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
30 dvn0 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
31 8 29 30 syl2anc 
 |-  ( ph -> ( ( S Dn F ) ` 0 ) = F )
32 31 dmeqd 
 |-  ( ph -> dom ( ( S Dn F ) ` 0 ) = dom F )
33 2 fdmd 
 |-  ( ph -> dom F = A )
34 32 33 eqtrd 
 |-  ( ph -> dom ( ( S Dn F ) ` 0 ) = A )
35 25 34 eleqtrd 
 |-  ( ph -> B e. A )
36 9 35 sseldd 
 |-  ( ph -> B e. CC )
37 cnfldbas 
 |-  CC = ( Base ` CCfld )
38 cnfld0 
 |-  0 = ( 0g ` CCfld )
39 cnring 
 |-  CCfld e. Ring
40 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
41 39 40 mp1i 
 |-  ( ph -> CCfld e. Mnd )
42 ovex 
 |-  ( 0 [,] N ) e. _V
43 42 inex1 
 |-  ( ( 0 [,] N ) i^i ZZ ) e. _V
44 43 a1i 
 |-  ( ph -> ( ( 0 [,] N ) i^i ZZ ) e. _V )
45 1 adantr 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> S e. { RR , CC } )
46 29 adantr 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> F e. ( CC ^pm S ) )
47 simpr 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ( ( 0 [,] N ) i^i ZZ ) )
48 47 elin2d 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ZZ )
49 47 elin1d 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. ( 0 [,] N ) )
50 nn0re 
 |-  ( N e. NN0 -> N e. RR )
51 50 rexrd 
 |-  ( N e. NN0 -> N e. RR* )
52 id 
 |-  ( N = +oo -> N = +oo )
53 pnfxr 
 |-  +oo e. RR*
54 52 53 eqeltrdi 
 |-  ( N = +oo -> N e. RR* )
55 51 54 jaoi 
 |-  ( ( N e. NN0 \/ N = +oo ) -> N e. RR* )
56 4 55 syl 
 |-  ( ph -> N e. RR* )
57 56 adantr 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> N e. RR* )
58 elicc1 
 |-  ( ( 0 e. RR* /\ N e. RR* ) -> ( k e. ( 0 [,] N ) <-> ( k e. RR* /\ 0 <_ k /\ k <_ N ) ) )
59 15 57 58 sylancr 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( k e. ( 0 [,] N ) <-> ( k e. RR* /\ 0 <_ k /\ k <_ N ) ) )
60 49 59 mpbid 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( k e. RR* /\ 0 <_ k /\ k <_ N ) )
61 60 simp2d 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> 0 <_ k )
62 elnn0z 
 |-  ( k e. NN0 <-> ( k e. ZZ /\ 0 <_ k ) )
63 48 61 62 sylanbrc 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> k e. NN0 )
64 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
65 45 46 63 64 syl3anc 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( S Dn F ) ` k ) : dom ( ( S Dn F ) ` k ) --> CC )
66 65 5 ffvelrnd 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( S Dn F ) ` k ) ` B ) e. CC )
67 63 faccld 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ! ` k ) e. NN )
68 67 nncnd 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ! ` k ) e. CC )
69 67 nnne0d 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ! ` k ) =/= 0 )
70 66 68 69 divcld 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. CC )
71 0cnd 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> 0 e. CC )
72 71 63 expcld 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( 0 ^ k ) e. CC )
73 70 72 mulcld 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) e. CC )
74 73 fmpttd 
 |-  ( ph -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) : ( ( 0 [,] N ) i^i ZZ ) --> CC )
75 eldifi 
 |-  ( k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) -> k e. ( ( 0 [,] N ) i^i ZZ ) )
76 75 63 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> k e. NN0 )
77 eldifsni 
 |-  ( k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) -> k =/= 0 )
78 77 adantl 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> k =/= 0 )
79 elnnne0 
 |-  ( k e. NN <-> ( k e. NN0 /\ k =/= 0 ) )
80 76 78 79 sylanbrc 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> k e. NN )
81 80 0expd 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> ( 0 ^ k ) = 0 )
82 81 oveq2d 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. 0 ) )
83 70 mul01d 
 |-  ( ( ph /\ k e. ( ( 0 [,] N ) i^i ZZ ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. 0 ) = 0 )
84 75 83 sylan2 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. 0 ) = 0 )
85 82 84 eqtrd 
 |-  ( ( ph /\ k e. ( ( ( 0 [,] N ) i^i ZZ ) \ { 0 } ) ) -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) = 0 )
86 zex 
 |-  ZZ e. _V
87 86 inex2 
 |-  ( ( 0 [,] N ) i^i ZZ ) e. _V
88 87 a1i 
 |-  ( ph -> ( ( 0 [,] N ) i^i ZZ ) e. _V )
89 85 88 suppss2 
 |-  ( ph -> ( ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) supp 0 ) C_ { 0 } )
90 37 38 41 44 24 74 89 gsumpt 
 |-  ( ph -> ( CCfld gsum ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ) = ( ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ` 0 ) )
91 10 fveq1d 
 |-  ( k = 0 -> ( ( ( S Dn F ) ` k ) ` B ) = ( ( ( S Dn F ) ` 0 ) ` B ) )
92 fveq2 
 |-  ( k = 0 -> ( ! ` k ) = ( ! ` 0 ) )
93 fac0 
 |-  ( ! ` 0 ) = 1
94 92 93 eqtrdi 
 |-  ( k = 0 -> ( ! ` k ) = 1 )
95 91 94 oveq12d 
 |-  ( k = 0 -> ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) = ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) )
96 oveq2 
 |-  ( k = 0 -> ( 0 ^ k ) = ( 0 ^ 0 ) )
97 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
98 96 97 eqtrdi 
 |-  ( k = 0 -> ( 0 ^ k ) = 1 )
99 95 98 oveq12d 
 |-  ( k = 0 -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) = ( ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) x. 1 ) )
100 eqid 
 |-  ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) = ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) )
101 ovex 
 |-  ( ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) x. 1 ) e. _V
102 99 100 101 fvmpt 
 |-  ( 0 e. ( ( 0 [,] N ) i^i ZZ ) -> ( ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ` 0 ) = ( ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) x. 1 ) )
103 24 102 syl 
 |-  ( ph -> ( ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ` 0 ) = ( ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) x. 1 ) )
104 31 fveq1d 
 |-  ( ph -> ( ( ( S Dn F ) ` 0 ) ` B ) = ( F ` B ) )
105 104 oveq1d 
 |-  ( ph -> ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) = ( ( F ` B ) / 1 ) )
106 2 35 ffvelrnd 
 |-  ( ph -> ( F ` B ) e. CC )
107 106 div1d 
 |-  ( ph -> ( ( F ` B ) / 1 ) = ( F ` B ) )
108 105 107 eqtrd 
 |-  ( ph -> ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) = ( F ` B ) )
109 108 oveq1d 
 |-  ( ph -> ( ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) x. 1 ) = ( ( F ` B ) x. 1 ) )
110 106 mulid1d 
 |-  ( ph -> ( ( F ` B ) x. 1 ) = ( F ` B ) )
111 109 110 eqtrd 
 |-  ( ph -> ( ( ( ( ( S Dn F ) ` 0 ) ` B ) / 1 ) x. 1 ) = ( F ` B ) )
112 90 103 111 3eqtrd 
 |-  ( ph -> ( CCfld gsum ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ) = ( F ` B ) )
113 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
114 39 113 mp1i 
 |-  ( ph -> CCfld e. CMnd )
115 cnfldtps 
 |-  CCfld e. TopSp
116 115 a1i 
 |-  ( ph -> CCfld e. TopSp )
117 mptexg 
 |-  ( ( ( 0 [,] N ) i^i ZZ ) e. _V -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) e. _V )
118 87 117 mp1i 
 |-  ( ph -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) e. _V )
119 funmpt 
 |-  Fun ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) )
120 119 a1i 
 |-  ( ph -> Fun ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) )
121 c0ex 
 |-  0 e. _V
122 121 a1i 
 |-  ( ph -> 0 e. _V )
123 snfi 
 |-  { 0 } e. Fin
124 123 a1i 
 |-  ( ph -> { 0 } e. Fin )
125 suppssfifsupp 
 |-  ( ( ( ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) e. _V /\ Fun ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) /\ 0 e. _V ) /\ ( { 0 } e. Fin /\ ( ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) supp 0 ) C_ { 0 } ) ) -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) finSupp 0 )
126 118 120 122 124 89 125 syl32anc 
 |-  ( ph -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) finSupp 0 )
127 37 38 114 116 44 74 126 tsmsid 
 |-  ( ph -> ( CCfld gsum ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ) e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ) )
128 112 127 eqeltrrd 
 |-  ( ph -> ( F ` B ) e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ) )
129 36 subidd 
 |-  ( ph -> ( B - B ) = 0 )
130 129 oveq1d 
 |-  ( ph -> ( ( B - B ) ^ k ) = ( 0 ^ k ) )
131 130 oveq2d 
 |-  ( ph -> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( B - B ) ^ k ) ) = ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) )
132 131 mpteq2dv 
 |-  ( ph -> ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( B - B ) ^ k ) ) ) = ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) )
133 132 oveq2d 
 |-  ( ph -> ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( B - B ) ^ k ) ) ) ) = ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( 0 ^ k ) ) ) ) )
134 128 133 eleqtrrd 
 |-  ( ph -> ( F ` B ) e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( B - B ) ^ k ) ) ) ) )
135 1 2 3 4 5 6 eltayl 
 |-  ( ph -> ( B T ( F ` B ) <-> ( B e. CC /\ ( F ` B ) e. ( CCfld tsums ( k e. ( ( 0 [,] N ) i^i ZZ ) |-> ( ( ( ( ( S Dn F ) ` k ) ` B ) / ( ! ` k ) ) x. ( ( B - B ) ^ k ) ) ) ) ) ) )
136 36 134 135 mpbir2and 
 |-  ( ph -> B T ( F ` B ) )
137 1 2 3 4 5 6 taylf 
 |-  ( ph -> T : dom T --> CC )
138 ffun 
 |-  ( T : dom T --> CC -> Fun T )
139 funbrfv2b 
 |-  ( Fun T -> ( B T ( F ` B ) <-> ( B e. dom T /\ ( T ` B ) = ( F ` B ) ) ) )
140 137 138 139 3syl 
 |-  ( ph -> ( B T ( F ` B ) <-> ( B e. dom T /\ ( T ` B ) = ( F ` B ) ) ) )
141 136 140 mpbid 
 |-  ( ph -> ( B e. dom T /\ ( T ` B ) = ( F ` B ) ) )