Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
โข (๐ โ UniOp โ ๐ โ V) |
2 | | fof 6753 |
. . . 4
โข (๐: โโontoโ โ โ ๐: โโถ โ) |
3 | | ax-hilex 29770 |
. . . 4
โข โ
โ V |
4 | | fex 7172 |
. . . 4
โข ((๐: โโถ โ โง
โ โ V) โ ๐
โ V) |
5 | 2, 3, 4 | sylancl 586 |
. . 3
โข (๐: โโontoโ โ โ ๐ โ V) |
6 | 5 | adantr 481 |
. 2
โข ((๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) โ ๐ โ V) |
7 | | foeq1 6749 |
. . . 4
โข (๐ก = ๐ โ (๐ก: โโontoโ โ โ ๐: โโontoโ โ)) |
8 | | fveq1 6838 |
. . . . . . 7
โข (๐ก = ๐ โ (๐กโ๐ฅ) = (๐โ๐ฅ)) |
9 | | fveq1 6838 |
. . . . . . 7
โข (๐ก = ๐ โ (๐กโ๐ฆ) = (๐โ๐ฆ)) |
10 | 8, 9 | oveq12d 7369 |
. . . . . 6
โข (๐ก = ๐ โ ((๐กโ๐ฅ) ยทih (๐กโ๐ฆ)) = ((๐โ๐ฅ) ยทih (๐โ๐ฆ))) |
11 | 10 | eqeq1d 2739 |
. . . . 5
โข (๐ก = ๐ โ (((๐กโ๐ฅ) ยทih (๐กโ๐ฆ)) = (๐ฅ ยทih ๐ฆ) โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) |
12 | 11 | 2ralbidv 3210 |
. . . 4
โข (๐ก = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ ((๐กโ๐ฅ) ยทih (๐กโ๐ฆ)) = (๐ฅ ยทih ๐ฆ) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) |
13 | 7, 12 | anbi12d 631 |
. . 3
โข (๐ก = ๐ โ ((๐ก: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐กโ๐ฅ) ยทih (๐กโ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)))) |
14 | | df-unop 30614 |
. . 3
โข UniOp =
{๐ก โฃ (๐ก: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐กโ๐ฅ) ยทih (๐กโ๐ฆ)) = (๐ฅ ยทih ๐ฆ))} |
15 | 13, 14 | elab2g 3630 |
. 2
โข (๐ โ V โ (๐ โ UniOp โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)))) |
16 | 1, 6, 15 | pm5.21nii 379 |
1
โข (๐ โ UniOp โ (๐: โโontoโ โ โง โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = (๐ฅ ยทih ๐ฆ))) |