Step | Hyp | Ref
| Expression |
1 | | funadj 31394 |
. 2
โข Fun
adjโ |
2 | | df-adjh 31357 |
. . . . . 6
โข
adjโ = {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐งโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)))} |
3 | 2 | eleq2i 2825 |
. . . . 5
โข
(โจ๐, ๐โฉ โ
adjโ โ โจ๐, ๐โฉ โ {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐งโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)))}) |
4 | | ax-hilex 30507 |
. . . . . . 7
โข โ
โ V |
5 | | fex 7230 |
. . . . . . 7
โข ((๐: โโถ โ โง
โ โ V) โ ๐
โ V) |
6 | 4, 5 | mpan2 689 |
. . . . . 6
โข (๐: โโถ โ โ
๐ โ
V) |
7 | | fex 7230 |
. . . . . . 7
โข ((๐: โโถ โ โง
โ โ V) โ ๐
โ V) |
8 | 4, 7 | mpan2 689 |
. . . . . 6
โข (๐: โโถ โ โ
๐ โ
V) |
9 | | feq1 6698 |
. . . . . . . 8
โข (๐ง = ๐ โ (๐ง: โโถ โ โ ๐: โโถ
โ)) |
10 | | fveq1 6890 |
. . . . . . . . . . 11
โข (๐ง = ๐ โ (๐งโ๐ฅ) = (๐โ๐ฅ)) |
11 | 10 | oveq1d 7426 |
. . . . . . . . . 10
โข (๐ง = ๐ โ ((๐งโ๐ฅ) ยทih ๐ฆ) = ((๐โ๐ฅ) ยทih ๐ฆ)) |
12 | 11 | eqeq1d 2734 |
. . . . . . . . 9
โข (๐ง = ๐ โ (((๐งโ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)))) |
13 | 12 | 2ralbidv 3218 |
. . . . . . . 8
โข (๐ง = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ ((๐งโ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)))) |
14 | 9, 13 | 3anbi13d 1438 |
. . . . . . 7
โข (๐ง = ๐ โ ((๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐งโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ))) โ (๐: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ))))) |
15 | | feq1 6698 |
. . . . . . . 8
โข (๐ค = ๐ โ (๐ค: โโถ โ โ ๐: โโถ
โ)) |
16 | | fveq1 6890 |
. . . . . . . . . . 11
โข (๐ค = ๐ โ (๐คโ๐ฆ) = (๐โ๐ฆ)) |
17 | 16 | oveq2d 7427 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (๐ฅ ยทih (๐คโ๐ฆ)) = (๐ฅ ยทih (๐โ๐ฆ))) |
18 | 17 | eqeq2d 2743 |
. . . . . . . . 9
โข (๐ค = ๐ โ (((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)) โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ)))) |
19 | 18 | 2ralbidv 3218 |
. . . . . . . 8
โข (๐ค = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)) โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ)))) |
20 | 15, 19 | 3anbi23d 1439 |
. . . . . . 7
โข (๐ค = ๐ โ ((๐: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ))) โ (๐: โโถ โ โง ๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))))) |
21 | 14, 20 | opelopabg 5538 |
. . . . . 6
โข ((๐ โ V โง ๐ โ V) โ (โจ๐, ๐โฉ โ {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐งโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)))} โ (๐: โโถ โ โง ๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))))) |
22 | 6, 8, 21 | syl2an 596 |
. . . . 5
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (โจ๐, ๐โฉ โ {โจ๐ง, ๐คโฉ โฃ (๐ง: โโถ โ โง ๐ค: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐งโ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐คโ๐ฆ)))} โ (๐: โโถ โ โง ๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))))) |
23 | 3, 22 | bitrid 282 |
. . . 4
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (โจ๐, ๐โฉ โ
adjโ โ (๐: โโถ โ โง ๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))))) |
24 | | df-3an 1089 |
. . . . 5
โข ((๐: โโถ โ โง
๐: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))) โ ((๐: โโถ โ โง ๐: โโถ โ) โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ)))) |
25 | 24 | baibr 537 |
. . . 4
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ)) โ (๐: โโถ โ โง ๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))))) |
26 | 23, 25 | bitr4d 281 |
. . 3
โข ((๐: โโถ โ โง
๐: โโถ โ)
โ (โจ๐, ๐โฉ โ
adjโ โ โ๐ฅ โ โ โ๐ฆ โ โ ((๐โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ)))) |
27 | 26 | biimp3ar 1470 |
. 2
โข ((๐: โโถ โ โง
๐: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))) โ โจ๐, ๐โฉ โ
adjโ) |
28 | | funopfv 6943 |
. 2
โข (Fun
adjโ โ (โจ๐, ๐โฉ โ adjโ โ
(adjโโ๐) = ๐)) |
29 | 1, 27, 28 | mpsyl 68 |
1
โข ((๐: โโถ โ โง
๐: โโถ โ
โง โ๐ฅ โ
โ โ๐ฆ โ
โ ((๐โ๐ฅ)
ยทih ๐ฆ) = (๐ฅ ยทih (๐โ๐ฆ))) โ
(adjโโ๐) = ๐) |