Step | Hyp | Ref
| Expression |
1 | | taylfval.a |
. . . . 5
β’ (π β π΄ β π) |
2 | | taylfval.s |
. . . . . 6
β’ (π β π β {β, β}) |
3 | | recnprss 25284 |
. . . . . 6
β’ (π β {β, β}
β π β
β) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ (π β π β β) |
5 | 1, 4 | sstrd 3959 |
. . . 4
β’ (π β π΄ β β) |
6 | | fveq2 6847 |
. . . . . . . 8
β’ (π = 0 β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)β0)) |
7 | 6 | dmeqd 5866 |
. . . . . . 7
β’ (π = 0 β dom ((π Dπ πΉ)βπ) = dom ((π Dπ πΉ)β0)) |
8 | 7 | eleq2d 2824 |
. . . . . 6
β’ (π = 0 β (π΅ β dom ((π Dπ πΉ)βπ) β π΅ β dom ((π Dπ πΉ)β0))) |
9 | | taylfval.b |
. . . . . . 7
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
10 | 9 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ)) |
11 | | taylfval.n |
. . . . . . . 8
β’ (π β (π β β0 β¨ π = +β)) |
12 | | elxnn0 12494 |
. . . . . . . . 9
β’ (π β
β0* β (π β β0 β¨ π = +β)) |
13 | | 0xr 11209 |
. . . . . . . . . . 11
β’ 0 β
β* |
14 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (π β
β0* β 0 β
β*) |
15 | | xnn0xr 12497 |
. . . . . . . . . 10
β’ (π β
β0* β π β
β*) |
16 | | xnn0ge0 13061 |
. . . . . . . . . 10
β’ (π β
β0* β 0 β€ π) |
17 | | lbicc2 13388 |
. . . . . . . . . 10
β’ ((0
β β* β§ π β β* β§ 0 β€
π) β 0 β
(0[,]π)) |
18 | 14, 15, 16, 17 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β
β0* β 0 β (0[,]π)) |
19 | 12, 18 | sylbir 234 |
. . . . . . . 8
β’ ((π β β0 β¨
π = +β) β 0
β (0[,]π)) |
20 | 11, 19 | syl 17 |
. . . . . . 7
β’ (π β 0 β (0[,]π)) |
21 | | 0zd 12518 |
. . . . . . 7
β’ (π β 0 β
β€) |
22 | 20, 21 | elind 4159 |
. . . . . 6
β’ (π β 0 β ((0[,]π) β©
β€)) |
23 | 8, 10, 22 | rspcdva 3585 |
. . . . 5
β’ (π β π΅ β dom ((π Dπ πΉ)β0)) |
24 | | cnex 11139 |
. . . . . . . . . 10
β’ β
β V |
25 | 24 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
V) |
26 | | taylfval.f |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆβ) |
27 | | elpm2r 8790 |
. . . . . . . . 9
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
28 | 25, 2, 26, 1, 27 | syl22anc 838 |
. . . . . . . 8
β’ (π β πΉ β (β βpm π)) |
29 | | dvn0 25304 |
. . . . . . . 8
β’ ((π β β β§ πΉ β (β
βpm π))
β ((π
Dπ πΉ)β0) = πΉ) |
30 | 4, 28, 29 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π Dπ πΉ)β0) = πΉ) |
31 | 30 | dmeqd 5866 |
. . . . . 6
β’ (π β dom ((π Dπ πΉ)β0) = dom πΉ) |
32 | 26 | fdmd 6684 |
. . . . . 6
β’ (π β dom πΉ = π΄) |
33 | 31, 32 | eqtrd 2777 |
. . . . 5
β’ (π β dom ((π Dπ πΉ)β0) = π΄) |
34 | 23, 33 | eleqtrd 2840 |
. . . 4
β’ (π β π΅ β π΄) |
35 | 5, 34 | sseldd 3950 |
. . 3
β’ (π β π΅ β β) |
36 | | cnfldbas 20816 |
. . . . . . 7
β’ β =
(Baseββfld) |
37 | | cnfld0 20837 |
. . . . . . 7
β’ 0 =
(0gββfld) |
38 | | cnring 20835 |
. . . . . . . 8
β’
βfld β Ring |
39 | | ringmnd 19981 |
. . . . . . . 8
β’
(βfld β Ring β βfld β
Mnd) |
40 | 38, 39 | mp1i 13 |
. . . . . . 7
β’ (π β βfld
β Mnd) |
41 | | ovex 7395 |
. . . . . . . . 9
β’
(0[,]π) β
V |
42 | 41 | inex1 5279 |
. . . . . . . 8
β’
((0[,]π) β©
β€) β V |
43 | 42 | a1i 11 |
. . . . . . 7
β’ (π β ((0[,]π) β© β€) β V) |
44 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((0[,]π) β© β€)) β π β {β, β}) |
45 | 28 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((0[,]π) β© β€)) β πΉ β (β βpm π)) |
46 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((0[,]π) β© β€)) β π β ((0[,]π) β© β€)) |
47 | 46 | elin2d 4164 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((0[,]π) β© β€)) β π β β€) |
48 | 46 | elin1d 4163 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((0[,]π) β© β€)) β π β (0[,]π)) |
49 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β π β
β) |
50 | 49 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β*) |
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = +β β π = +β) |
52 | | pnfxr 11216 |
. . . . . . . . . . . . . . . . . . . 20
β’ +β
β β* |
53 | 51, 52 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = +β β π β
β*) |
54 | 50, 53 | jaoi 856 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0 β¨
π = +β) β π β
β*) |
55 | 11, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β
β*) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((0[,]π) β© β€)) β π β
β*) |
57 | | elicc1 13315 |
. . . . . . . . . . . . . . . 16
β’ ((0
β β* β§ π β β*) β (π β (0[,]π) β (π β β* β§ 0 β€
π β§ π β€ π))) |
58 | 13, 56, 57 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((0[,]π) β© β€)) β (π β (0[,]π) β (π β β* β§ 0 β€
π β§ π β€ π))) |
59 | 48, 58 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((0[,]π) β© β€)) β (π β β* β§ 0 β€
π β§ π β€ π)) |
60 | 59 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((0[,]π) β© β€)) β 0 β€ π) |
61 | | elnn0z 12519 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π β β€
β§ 0 β€ π)) |
62 | 47, 60, 61 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((0[,]π) β© β€)) β π β β0) |
63 | | dvnf 25307 |
. . . . . . . . . . . 12
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
64 | 44, 45, 62, 63 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β ((0[,]π) β© β€)) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
65 | 64, 9 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β ((0[,]π) β© β€)) β (((π Dπ πΉ)βπ)βπ΅) β β) |
66 | 62 | faccld 14191 |
. . . . . . . . . . 11
β’ ((π β§ π β ((0[,]π) β© β€)) β (!βπ) β
β) |
67 | 66 | nncnd 12176 |
. . . . . . . . . 10
β’ ((π β§ π β ((0[,]π) β© β€)) β (!βπ) β
β) |
68 | 66 | nnne0d 12210 |
. . . . . . . . . 10
β’ ((π β§ π β ((0[,]π) β© β€)) β (!βπ) β 0) |
69 | 65, 67, 68 | divcld 11938 |
. . . . . . . . 9
β’ ((π β§ π β ((0[,]π) β© β€)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β β) |
70 | | 0cnd 11155 |
. . . . . . . . . 10
β’ ((π β§ π β ((0[,]π) β© β€)) β 0 β
β) |
71 | 70, 62 | expcld 14058 |
. . . . . . . . 9
β’ ((π β§ π β ((0[,]π) β© β€)) β (0βπ) β
β) |
72 | 69, 71 | mulcld 11182 |
. . . . . . . 8
β’ ((π β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)) β β) |
73 | 72 | fmpttd 7068 |
. . . . . . 7
β’ (π β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))):((0[,]π) β©
β€)βΆβ) |
74 | | eldifi 4091 |
. . . . . . . . . . . . 13
β’ (π β (((0[,]π) β© β€) β {0}) β π β ((0[,]π) β© β€)) |
75 | 74, 62 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β π β
β0) |
76 | | eldifsni 4755 |
. . . . . . . . . . . . 13
β’ (π β (((0[,]π) β© β€) β {0}) β π β 0) |
77 | 76 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β π β 0) |
78 | | elnnne0 12434 |
. . . . . . . . . . . 12
β’ (π β β β (π β β0
β§ π β
0)) |
79 | 75, 77, 78 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β π β
β) |
80 | 79 | 0expd 14051 |
. . . . . . . . . 10
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β
(0βπ) =
0) |
81 | 80 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)) = (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· 0)) |
82 | 69 | mul01d 11361 |
. . . . . . . . . 10
β’ ((π β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· 0) = 0) |
83 | 74, 82 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· 0) = 0) |
84 | 81, 83 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π β (((0[,]π) β© β€) β {0})) β
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)) = 0) |
85 | | zex 12515 |
. . . . . . . . . 10
β’ β€
β V |
86 | 85 | inex2 5280 |
. . . . . . . . 9
β’
((0[,]π) β©
β€) β V |
87 | 86 | a1i 11 |
. . . . . . . 8
β’ (π β ((0[,]π) β© β€) β V) |
88 | 84, 87 | suppss2 8136 |
. . . . . . 7
β’ (π β ((π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) supp 0) β {0}) |
89 | 36, 37, 40, 43, 22, 73, 88 | gsumpt 19746 |
. . . . . 6
β’ (π β (βfld
Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))) = ((π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))β0)) |
90 | 6 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π = 0 β (((π Dπ πΉ)βπ)βπ΅) = (((π Dπ πΉ)β0)βπ΅)) |
91 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = 0 β (!βπ) =
(!β0)) |
92 | | fac0 14183 |
. . . . . . . . . . 11
β’
(!β0) = 1 |
93 | 91, 92 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π = 0 β (!βπ) = 1) |
94 | 90, 93 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = 0 β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) = ((((π Dπ πΉ)β0)βπ΅) / 1)) |
95 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = 0 β (0βπ) = (0β0)) |
96 | | 0exp0e1 13979 |
. . . . . . . . . 10
β’
(0β0) = 1 |
97 | 95, 96 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π = 0 β (0βπ) = 1) |
98 | 94, 97 | oveq12d 7380 |
. . . . . . . 8
β’ (π = 0 β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)) = (((((π Dπ πΉ)β0)βπ΅) / 1) Β· 1)) |
99 | | eqid 2737 |
. . . . . . . 8
β’ (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) = (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) |
100 | | ovex 7395 |
. . . . . . . 8
β’
(((((π
Dπ πΉ)β0)βπ΅) / 1) Β· 1) β V |
101 | 98, 99, 100 | fvmpt 6953 |
. . . . . . 7
β’ (0 β
((0[,]π) β© β€)
β ((π β
((0[,]π) β© β€)
β¦ (((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))β0) = (((((π Dπ πΉ)β0)βπ΅) / 1) Β· 1)) |
102 | 22, 101 | syl 17 |
. . . . . 6
β’ (π β ((π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))β0) = (((((π Dπ πΉ)β0)βπ΅) / 1) Β· 1)) |
103 | 30 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π β (((π Dπ πΉ)β0)βπ΅) = (πΉβπ΅)) |
104 | 103 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β ((((π Dπ πΉ)β0)βπ΅) / 1) = ((πΉβπ΅) / 1)) |
105 | 26, 34 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (π β (πΉβπ΅) β β) |
106 | 105 | div1d 11930 |
. . . . . . . . 9
β’ (π β ((πΉβπ΅) / 1) = (πΉβπ΅)) |
107 | 104, 106 | eqtrd 2777 |
. . . . . . . 8
β’ (π β ((((π Dπ πΉ)β0)βπ΅) / 1) = (πΉβπ΅)) |
108 | 107 | oveq1d 7377 |
. . . . . . 7
β’ (π β (((((π Dπ πΉ)β0)βπ΅) / 1) Β· 1) = ((πΉβπ΅) Β· 1)) |
109 | 105 | mulid1d 11179 |
. . . . . . 7
β’ (π β ((πΉβπ΅) Β· 1) = (πΉβπ΅)) |
110 | 108, 109 | eqtrd 2777 |
. . . . . 6
β’ (π β (((((π Dπ πΉ)β0)βπ΅) / 1) Β· 1) = (πΉβπ΅)) |
111 | 89, 102, 110 | 3eqtrd 2781 |
. . . . 5
β’ (π β (βfld
Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))) = (πΉβπ΅)) |
112 | | ringcmn 20010 |
. . . . . . 7
β’
(βfld β Ring β βfld β
CMnd) |
113 | 38, 112 | mp1i 13 |
. . . . . 6
β’ (π β βfld
β CMnd) |
114 | | cnfldtps 24157 |
. . . . . . 7
β’
βfld β TopSp |
115 | 114 | a1i 11 |
. . . . . 6
β’ (π β βfld
β TopSp) |
116 | | mptexg 7176 |
. . . . . . . 8
β’
(((0[,]π) β©
β€) β V β (π
β ((0[,]π) β©
β€) β¦ (((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) β V) |
117 | 86, 116 | mp1i 13 |
. . . . . . 7
β’ (π β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) β V) |
118 | | funmpt 6544 |
. . . . . . . 8
β’ Fun
(π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) |
119 | 118 | a1i 11 |
. . . . . . 7
β’ (π β Fun (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))) |
120 | | c0ex 11156 |
. . . . . . . 8
β’ 0 β
V |
121 | 120 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
V) |
122 | | snfi 8995 |
. . . . . . . 8
β’ {0}
β Fin |
123 | 122 | a1i 11 |
. . . . . . 7
β’ (π β {0} β
Fin) |
124 | | suppssfifsupp 9327 |
. . . . . . 7
β’ ((((π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) β V β§ Fun (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) β§ 0 β V) β§ ({0} β Fin
β§ ((π β
((0[,]π) β© β€)
β¦ (((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) supp 0) β {0})) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) finSupp 0) |
125 | 117, 119,
121, 123, 88, 124 | syl32anc 1379 |
. . . . . 6
β’ (π β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) finSupp 0) |
126 | 36, 37, 113, 115, 43, 73, 125 | tsmsid 23507 |
. . . . 5
β’ (π β (βfld
Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))) β (βfld tsums
(π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))))) |
127 | 111, 126 | eqeltrrd 2839 |
. . . 4
β’ (π β (πΉβπ΅) β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))))) |
128 | 35 | subidd 11507 |
. . . . . . . 8
β’ (π β (π΅ β π΅) = 0) |
129 | 128 | oveq1d 7377 |
. . . . . . 7
β’ (π β ((π΅ β π΅)βπ) = (0βπ)) |
130 | 129 | oveq2d 7378 |
. . . . . 6
β’ (π β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π΅ β π΅)βπ)) = (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))) |
131 | 130 | mpteq2dv 5212 |
. . . . 5
β’ (π β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π΅ β π΅)βπ))) = (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ)))) |
132 | 131 | oveq2d 7378 |
. . . 4
β’ (π β (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π΅ β π΅)βπ)))) = (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (0βπ))))) |
133 | 127, 132 | eleqtrrd 2841 |
. . 3
β’ (π β (πΉβπ΅) β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π΅ β π΅)βπ))))) |
134 | | taylfval.t |
. . . 4
β’ π = (π(π Tayl πΉ)π΅) |
135 | 2, 26, 1, 11, 9, 134 | eltayl 25735 |
. . 3
β’ (π β (π΅π(πΉβπ΅) β (π΅ β β β§ (πΉβπ΅) β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π΅ β π΅)βπ))))))) |
136 | 35, 133, 135 | mpbir2and 712 |
. 2
β’ (π β π΅π(πΉβπ΅)) |
137 | 2, 26, 1, 11, 9, 134 | taylf 25736 |
. . 3
β’ (π β π:dom πβΆβ) |
138 | | ffun 6676 |
. . 3
β’ (π:dom πβΆβ β Fun π) |
139 | | funbrfv2b 6905 |
. . 3
β’ (Fun
π β (π΅π(πΉβπ΅) β (π΅ β dom π β§ (πβπ΅) = (πΉβπ΅)))) |
140 | 137, 138,
139 | 3syl 18 |
. 2
β’ (π β (π΅π(πΉβπ΅) β (π΅ β dom π β§ (πβπ΅) = (πΉβπ΅)))) |
141 | 136, 140 | mpbid 231 |
1
β’ (π β (π΅ β dom π β§ (πβπ΅) = (πΉβπ΅))) |