Step | Hyp | Ref
| Expression |
1 | | evlf2.l |
. 2
โข ๐ฟ = (โจ๐น, ๐โฉ(2nd โ๐ธ)โจ๐บ, ๐โฉ) |
2 | | evlfval.e |
. . . . 5
โข ๐ธ = (๐ถ evalF ๐ท) |
3 | | evlfval.c |
. . . . 5
โข (๐ โ ๐ถ โ Cat) |
4 | | evlfval.d |
. . . . 5
โข (๐ โ ๐ท โ Cat) |
5 | | evlfval.b |
. . . . 5
โข ๐ต = (Baseโ๐ถ) |
6 | | evlfval.h |
. . . . 5
โข ๐ป = (Hom โ๐ถ) |
7 | | evlfval.o |
. . . . 5
โข ยท =
(compโ๐ท) |
8 | | evlfval.n |
. . . . 5
โข ๐ = (๐ถ Nat ๐ท) |
9 | 2, 3, 4, 5, 6, 7, 8 | evlfval 18066 |
. . . 4
โข (๐ โ ๐ธ = โจ(๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ) |
10 | | ovex 7384 |
. . . . . 6
โข (๐ถ Func ๐ท) โ V |
11 | 5 | fvexi 6853 |
. . . . . 6
โข ๐ต โ V |
12 | 10, 11 | mpoex 8004 |
. . . . 5
โข (๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)) โ V |
13 | 10, 11 | xpex 7679 |
. . . . . 6
โข ((๐ถ Func ๐ท) ร ๐ต) โ V |
14 | 13, 13 | mpoex 8004 |
. . . . 5
โข (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐)))) โ V |
15 | 12, 14 | op2ndd 7924 |
. . . 4
โข (๐ธ = โจ(๐ โ (๐ถ Func ๐ท), ๐ฅ โ ๐ต โฆ ((1st โ๐)โ๐ฅ)), (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))โฉ โ
(2nd โ๐ธ) =
(๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))) |
16 | 9, 15 | syl 17 |
. . 3
โข (๐ โ (2nd
โ๐ธ) = (๐ฅ โ ((๐ถ Func ๐ท) ร ๐ต), ๐ฆ โ ((๐ถ Func ๐ท) ร ๐ต) โฆ โฆ(1st
โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))))) |
17 | | fvexd 6854 |
. . . 4
โข ((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โ (1st โ๐ฅ) โ V) |
18 | | simprl 769 |
. . . . . 6
โข ((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โ ๐ฅ = โจ๐น, ๐โฉ) |
19 | 18 | fveq2d 6843 |
. . . . 5
โข ((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โ (1st โ๐ฅ) = (1st
โโจ๐น, ๐โฉ)) |
20 | | evlf2.f |
. . . . . . 7
โข (๐ โ ๐น โ (๐ถ Func ๐ท)) |
21 | | evlf2.x |
. . . . . . 7
โข (๐ โ ๐ โ ๐ต) |
22 | | op1stg 7925 |
. . . . . . 7
โข ((๐น โ (๐ถ Func ๐ท) โง ๐ โ ๐ต) โ (1st โโจ๐น, ๐โฉ) = ๐น) |
23 | 20, 21, 22 | syl2anc 584 |
. . . . . 6
โข (๐ โ (1st
โโจ๐น, ๐โฉ) = ๐น) |
24 | 23 | adantr 481 |
. . . . 5
โข ((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โ (1st
โโจ๐น, ๐โฉ) = ๐น) |
25 | 19, 24 | eqtrd 2777 |
. . . 4
โข ((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โ (1st โ๐ฅ) = ๐น) |
26 | | fvexd 6854 |
. . . . 5
โข (((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โ (1st โ๐ฆ) โ V) |
27 | | simplrr 776 |
. . . . . . 7
โข (((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โ ๐ฆ = โจ๐บ, ๐โฉ) |
28 | 27 | fveq2d 6843 |
. . . . . 6
โข (((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โ (1st โ๐ฆ) = (1st
โโจ๐บ, ๐โฉ)) |
29 | | evlf2.g |
. . . . . . . 8
โข (๐ โ ๐บ โ (๐ถ Func ๐ท)) |
30 | | evlf2.y |
. . . . . . . 8
โข (๐ โ ๐ โ ๐ต) |
31 | | op1stg 7925 |
. . . . . . . 8
โข ((๐บ โ (๐ถ Func ๐ท) โง ๐ โ ๐ต) โ (1st โโจ๐บ, ๐โฉ) = ๐บ) |
32 | 29, 30, 31 | syl2anc 584 |
. . . . . . 7
โข (๐ โ (1st
โโจ๐บ, ๐โฉ) = ๐บ) |
33 | 32 | ad2antrr 724 |
. . . . . 6
โข (((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โ (1st โโจ๐บ, ๐โฉ) = ๐บ) |
34 | 28, 33 | eqtrd 2777 |
. . . . 5
โข (((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โ (1st โ๐ฆ) = ๐บ) |
35 | | simplr 767 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ๐ = ๐น) |
36 | | simpr 485 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ๐ = ๐บ) |
37 | 35, 36 | oveq12d 7369 |
. . . . . 6
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐๐๐) = (๐น๐๐บ)) |
38 | 18 | ad2antrr 724 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ๐ฅ = โจ๐น, ๐โฉ) |
39 | 38 | fveq2d 6843 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โ๐ฅ) = (2nd
โโจ๐น, ๐โฉ)) |
40 | | op2ndg 7926 |
. . . . . . . . . 10
โข ((๐น โ (๐ถ Func ๐ท) โง ๐ โ ๐ต) โ (2nd โโจ๐น, ๐โฉ) = ๐) |
41 | 20, 21, 40 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ (2nd
โโจ๐น, ๐โฉ) = ๐) |
42 | 41 | ad3antrrr 728 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โโจ๐น, ๐โฉ) = ๐) |
43 | 39, 42 | eqtrd 2777 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โ๐ฅ) = ๐) |
44 | 27 | adantr 481 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ๐ฆ = โจ๐บ, ๐โฉ) |
45 | 44 | fveq2d 6843 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โ๐ฆ) = (2nd
โโจ๐บ, ๐โฉ)) |
46 | | op2ndg 7926 |
. . . . . . . . . 10
โข ((๐บ โ (๐ถ Func ๐ท) โง ๐ โ ๐ต) โ (2nd โโจ๐บ, ๐โฉ) = ๐) |
47 | 29, 30, 46 | syl2anc 584 |
. . . . . . . . 9
โข (๐ โ (2nd
โโจ๐บ, ๐โฉ) = ๐) |
48 | 47 | ad3antrrr 728 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โโจ๐บ, ๐โฉ) = ๐) |
49 | 45, 48 | eqtrd 2777 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โ๐ฆ) = ๐) |
50 | 43, 49 | oveq12d 7369 |
. . . . . 6
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) = (๐๐ป๐)) |
51 | 35 | fveq2d 6843 |
. . . . . . . . . 10
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (1st โ๐) = (1st โ๐น)) |
52 | 51, 43 | fveq12d 6846 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((1st โ๐)โ(2nd
โ๐ฅ)) =
((1st โ๐น)โ๐)) |
53 | 51, 49 | fveq12d 6846 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((1st โ๐)โ(2nd
โ๐ฆ)) =
((1st โ๐น)โ๐)) |
54 | 52, 53 | opeq12d 4836 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ โจ((1st โ๐)โ(2nd
โ๐ฅ)),
((1st โ๐)โ(2nd โ๐ฆ))โฉ =
โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ) |
55 | 36 | fveq2d 6843 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (1st โ๐) = (1st โ๐บ)) |
56 | 55, 49 | fveq12d 6846 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((1st โ๐)โ(2nd
โ๐ฆ)) =
((1st โ๐บ)โ๐)) |
57 | 54, 56 | oveq12d 7369 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ))) = (โจ((1st
โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))) |
58 | 49 | fveq2d 6843 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐โ(2nd โ๐ฆ)) = (๐โ๐)) |
59 | 35 | fveq2d 6843 |
. . . . . . . . 9
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (2nd โ๐) = (2nd โ๐น)) |
60 | 59, 43, 49 | oveq123d 7372 |
. . . . . . . 8
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ)) = (๐(2nd โ๐น)๐)) |
61 | 60 | fveq1d 6841 |
. . . . . . 7
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (((2nd โ๐ฅ)(2nd โ๐)(2nd โ๐ฆ))โ๐) = ((๐(2nd โ๐น)๐)โ๐)) |
62 | 57, 58, 61 | oveq123d 7372 |
. . . . . 6
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐)) = ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐))) |
63 | 37, 50, 62 | mpoeq123dv 7426 |
. . . . 5
โข ((((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โง ๐ = ๐บ) โ (๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))) = (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐)))) |
64 | 26, 34, 63 | csbied2 3893 |
. . . 4
โข (((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โง ๐ = ๐น) โ โฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))) = (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐)))) |
65 | 17, 25, 64 | csbied2 3893 |
. . 3
โข ((๐ โง (๐ฅ = โจ๐น, ๐โฉ โง ๐ฆ = โจ๐บ, ๐โฉ)) โ
โฆ(1st โ๐ฅ) / ๐โฆโฆ(1st
โ๐ฆ) / ๐โฆ(๐ โ (๐๐๐), ๐ โ ((2nd โ๐ฅ)๐ป(2nd โ๐ฆ)) โฆ ((๐โ(2nd โ๐ฆ))(โจ((1st
โ๐)โ(2nd โ๐ฅ)), ((1st
โ๐)โ(2nd โ๐ฆ))โฉ ยท ((1st
โ๐)โ(2nd โ๐ฆ)))(((2nd
โ๐ฅ)(2nd
โ๐)(2nd
โ๐ฆ))โ๐))) = (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐)))) |
66 | 20, 21 | opelxpd 5669 |
. . 3
โข (๐ โ โจ๐น, ๐โฉ โ ((๐ถ Func ๐ท) ร ๐ต)) |
67 | 29, 30 | opelxpd 5669 |
. . 3
โข (๐ โ โจ๐บ, ๐โฉ โ ((๐ถ Func ๐ท) ร ๐ต)) |
68 | | ovex 7384 |
. . . . 5
โข (๐น๐๐บ) โ V |
69 | | ovex 7384 |
. . . . 5
โข (๐๐ป๐) โ V |
70 | 68, 69 | mpoex 8004 |
. . . 4
โข (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐))) โ V |
71 | 70 | a1i 11 |
. . 3
โข (๐ โ (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐))) โ V) |
72 | 16, 65, 66, 67, 71 | ovmpod 7501 |
. 2
โข (๐ โ (โจ๐น, ๐โฉ(2nd โ๐ธ)โจ๐บ, ๐โฉ) = (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐)))) |
73 | 1, 72 | eqtrid 2789 |
1
โข (๐ โ ๐ฟ = (๐ โ (๐น๐๐บ), ๐ โ (๐๐ป๐) โฆ ((๐โ๐)(โจ((1st โ๐น)โ๐), ((1st โ๐น)โ๐)โฉ ยท ((1st
โ๐บ)โ๐))((๐(2nd โ๐น)๐)โ๐)))) |