Step | Hyp | Ref
| Expression |
1 | | opex 5421 |
. . . . . . . . 9
โข
โจ(๐นโ๐), (๐นโ๐)โฉ โ V |
2 | | fvex 6855 |
. . . . . . . . 9
โข (๐นโ(๐ ยท ๐)) โ V |
3 | 1, 2 | relsnop 5761 |
. . . . . . . 8
โข Rel
{โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} |
4 | 3 | rgenw 3068 |
. . . . . . 7
โข
โ๐ โ
๐ Rel {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} |
5 | | reliun 5772 |
. . . . . . 7
โข (Rel
โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ๐ โ ๐ Rel {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
6 | 4, 5 | mpbir 230 |
. . . . . 6
โข Rel
โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} |
7 | 6 | rgenw 3068 |
. . . . 5
โข
โ๐ โ
๐ Rel โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} |
8 | | reliun 5772 |
. . . . 5
โข (Rel
โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ๐ โ ๐ Rel โช
๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
9 | 7, 8 | mpbir 230 |
. . . 4
โข Rel
โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} |
10 | | imasaddflem.a |
. . . . 5
โข (๐ โ โ = โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
11 | 10 | releqd 5734 |
. . . 4
โข (๐ โ (Rel โ โ Rel โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ})) |
12 | 9, 11 | mpbiri 257 |
. . 3
โข (๐ โ Rel โ ) |
13 | | imasaddf.f |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐น:๐โontoโ๐ต) |
14 | | fof 6756 |
. . . . . . . . . . . . . . . 16
โข (๐น:๐โontoโ๐ต โ ๐น:๐โถ๐ต) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐น:๐โถ๐ต) |
16 | | ffvelcdm 7032 |
. . . . . . . . . . . . . . . 16
โข ((๐น:๐โถ๐ต โง ๐ โ ๐) โ (๐นโ๐) โ ๐ต) |
17 | | ffvelcdm 7032 |
. . . . . . . . . . . . . . . 16
โข ((๐น:๐โถ๐ต โง ๐ โ ๐) โ (๐นโ๐) โ ๐ต) |
18 | 16, 17 | anim12dan 619 |
. . . . . . . . . . . . . . 15
โข ((๐น:๐โถ๐ต โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐นโ๐) โ ๐ต โง (๐นโ๐) โ ๐ต)) |
19 | 15, 18 | sylan 580 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐นโ๐) โ ๐ต โง (๐นโ๐) โ ๐ต)) |
20 | | opelxpi 5670 |
. . . . . . . . . . . . . 14
โข (((๐นโ๐) โ ๐ต โง (๐นโ๐) โ ๐ต) โ โจ(๐นโ๐), (๐นโ๐)โฉ โ (๐ต ร ๐ต)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ โจ(๐นโ๐), (๐นโ๐)โฉ โ (๐ต ร ๐ต)) |
22 | | opelxpi 5670 |
. . . . . . . . . . . . 13
โข
((โจ(๐นโ๐), (๐นโ๐)โฉ โ (๐ต ร ๐ต) โง (๐นโ(๐ ยท ๐)) โ V) โ โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ ((๐ต ร ๐ต) ร V)) |
23 | 21, 2, 22 | sylancl 586 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ ((๐ต ร ๐ต) ร V)) |
24 | 23 | snssd 4769 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ((๐ต ร ๐ต) ร V)) |
25 | 24 | anassrs 468 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ((๐ต ร ๐ต) ร V)) |
26 | 25 | iunssd 5010 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ โช
๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ((๐ต ร ๐ต) ร V)) |
27 | 26 | iunssd 5010 |
. . . . . . . 8
โข (๐ โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ((๐ต ร ๐ต) ร V)) |
28 | 10, 27 | eqsstrd 3982 |
. . . . . . 7
โข (๐ โ โ โ ((๐ต ร ๐ต) ร V)) |
29 | | dmss 5858 |
. . . . . . 7
โข ( โ
โ ((๐ต ร ๐ต) ร V) โ dom โ
โ dom ((๐ต ร
๐ต) ร
V)) |
30 | 28, 29 | syl 17 |
. . . . . 6
โข (๐ โ dom โ โ dom ((๐ต ร ๐ต) ร V)) |
31 | | vn0 4298 |
. . . . . . 7
โข V โ
โ
|
32 | | dmxp 5884 |
. . . . . . 7
โข (V โ
โ
โ dom ((๐ต
ร ๐ต) ร V) =
(๐ต ร ๐ต)) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
โข dom
((๐ต ร ๐ต) ร V) = (๐ต ร ๐ต) |
34 | 30, 33 | sseqtrdi 3994 |
. . . . 5
โข (๐ โ dom โ โ (๐ต ร ๐ต)) |
35 | | forn 6759 |
. . . . . . 7
โข (๐น:๐โontoโ๐ต โ ran ๐น = ๐ต) |
36 | 13, 35 | syl 17 |
. . . . . 6
โข (๐ โ ran ๐น = ๐ต) |
37 | 36 | sqxpeqd 5665 |
. . . . 5
โข (๐ โ (ran ๐น ร ran ๐น) = (๐ต ร ๐ต)) |
38 | 34, 37 | sseqtrrd 3985 |
. . . 4
โข (๐ โ dom โ โ (ran ๐น ร ran ๐น)) |
39 | 10 | eleq2d 2823 |
. . . . . . . . . . . . 13
โข (๐ โ (โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โ โ
โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ})) |
40 | 39 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โ โ
โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ})) |
41 | | df-br 5106 |
. . . . . . . . . . . 12
โข
(โจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค โ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โ ) |
42 | | eliun 4958 |
. . . . . . . . . . . . 13
โข
(โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ๐ โ ๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
43 | | eliun 4958 |
. . . . . . . . . . . . . 14
โข
(โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ๐ โ ๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
44 | 43 | rexbii 3097 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ๐ โ ๐ โ๐ โ ๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
45 | 42, 44 | bitr2i 275 |
. . . . . . . . . . . 12
โข
(โ๐ โ
๐ โ๐ โ ๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ}) |
46 | 40, 41, 45 | 3bitr4g 313 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค โ โ๐ โ ๐ โ๐ โ ๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ})) |
47 | | opex 5421 |
. . . . . . . . . . . . . . 15
โข
โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ V |
48 | 47 | elsn 4601 |
. . . . . . . . . . . . . 14
โข
(โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ = โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ) |
49 | | opex 5421 |
. . . . . . . . . . . . . . . 16
โข
โจ(๐นโ๐), (๐นโ๐)โฉ โ V |
50 | | vex 3449 |
. . . . . . . . . . . . . . . 16
โข ๐ค โ V |
51 | 49, 50 | opth 5433 |
. . . . . . . . . . . . . . 15
โข
(โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ = โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ (โจ(๐นโ๐), (๐นโ๐)โฉ = โจ(๐นโ๐), (๐นโ๐)โฉ โง ๐ค = (๐นโ(๐ ยท ๐)))) |
52 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . 19
โข (๐นโ๐) โ V |
53 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . 19
โข (๐นโ๐) โ V |
54 | 52, 53 | opth 5433 |
. . . . . . . . . . . . . . . . . 18
โข
(โจ(๐นโ๐), (๐นโ๐)โฉ = โจ(๐นโ๐), (๐นโ๐)โฉ โ ((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐))) |
55 | | imasaddf.e |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)))) |
56 | 54, 55 | biimtrid 241 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจ(๐นโ๐), (๐นโ๐)โฉ = โจ(๐นโ๐), (๐นโ๐)โฉ โ (๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)))) |
57 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . . 18
โข ((๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)) โ (๐ค = (๐นโ(๐ ยท ๐)) โ ๐ค = (๐นโ(๐ ยท ๐)))) |
58 | 57 | biimprd 247 |
. . . . . . . . . . . . . . . . 17
โข ((๐นโ(๐ ยท ๐)) = (๐นโ(๐ ยท ๐)) โ (๐ค = (๐นโ(๐ ยท ๐)) โ ๐ค = (๐นโ(๐ ยท ๐)))) |
59 | 56, 58 | syl6 35 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจ(๐นโ๐), (๐นโ๐)โฉ = โจ(๐นโ๐), (๐นโ๐)โฉ โ (๐ค = (๐นโ(๐ ยท ๐)) โ ๐ค = (๐นโ(๐ ยท ๐))))) |
60 | 59 | impd 411 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((โจ(๐นโ๐), (๐นโ๐)โฉ = โจ(๐นโ๐), (๐นโ๐)โฉ โง ๐ค = (๐นโ(๐ ยท ๐))) โ ๐ค = (๐นโ(๐ ยท ๐)))) |
61 | 51, 60 | biimtrid 241 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ = โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ ๐ค = (๐นโ(๐ ยท ๐)))) |
62 | 48, 61 | biimtrid 241 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ๐ค = (๐นโ(๐ ยท ๐)))) |
63 | 62 | 3expa 1118 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ๐ค = (๐นโ(๐ ยท ๐)))) |
64 | 63 | rexlimdvva 3205 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (โ๐ โ ๐ โ๐ โ ๐ โจโจ(๐นโ๐), (๐นโ๐)โฉ, ๐คโฉ โ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ ๐ค = (๐นโ(๐ ยท ๐)))) |
65 | 46, 64 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ (โจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค โ ๐ค = (๐นโ(๐ ยท ๐)))) |
66 | 65 | alrimiv 1930 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ โ๐ค(โจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค โ ๐ค = (๐นโ(๐ ยท ๐)))) |
67 | | mo2icl 3672 |
. . . . . . . . 9
โข
(โ๐ค(โจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค โ ๐ค = (๐นโ(๐ ยท ๐))) โ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐)) โ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค) |
69 | 68 | ralrimivva 3197 |
. . . . . . 7
โข (๐ โ โ๐ โ ๐ โ๐ โ ๐ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค) |
70 | | fofn 6758 |
. . . . . . . . . 10
โข (๐น:๐โontoโ๐ต โ ๐น Fn ๐) |
71 | 13, 70 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐น Fn ๐) |
72 | | opeq2 4831 |
. . . . . . . . . . . 12
โข (๐ง = (๐นโ๐) โ โจ(๐นโ๐), ๐งโฉ = โจ(๐นโ๐), (๐นโ๐)โฉ) |
73 | 72 | breq1d 5115 |
. . . . . . . . . . 11
โข (๐ง = (๐นโ๐) โ (โจ(๐นโ๐), ๐งโฉ โ ๐ค โ โจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค)) |
74 | 73 | mobidv 2547 |
. . . . . . . . . 10
โข (๐ง = (๐นโ๐) โ (โ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค โ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค)) |
75 | 74 | ralrn 7038 |
. . . . . . . . 9
โข (๐น Fn ๐ โ (โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค โ โ๐ โ ๐ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค)) |
76 | 71, 75 | syl 17 |
. . . . . . . 8
โข (๐ โ (โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค โ โ๐ โ ๐ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค)) |
77 | 76 | ralbidv 3174 |
. . . . . . 7
โข (๐ โ (โ๐ โ ๐ โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค โ โ๐ โ ๐ โ๐ โ ๐ โ*๐คโจ(๐นโ๐), (๐นโ๐)โฉ โ ๐ค)) |
78 | 69, 77 | mpbird 256 |
. . . . . 6
โข (๐ โ โ๐ โ ๐ โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค) |
79 | | opeq1 4830 |
. . . . . . . . . . 11
โข (๐ฆ = (๐นโ๐) โ โจ๐ฆ, ๐งโฉ = โจ(๐นโ๐), ๐งโฉ) |
80 | 79 | breq1d 5115 |
. . . . . . . . . 10
โข (๐ฆ = (๐นโ๐) โ (โจ๐ฆ, ๐งโฉ โ ๐ค โ โจ(๐นโ๐), ๐งโฉ โ ๐ค)) |
81 | 80 | mobidv 2547 |
. . . . . . . . 9
โข (๐ฆ = (๐นโ๐) โ (โ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค โ โ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค)) |
82 | 81 | ralbidv 3174 |
. . . . . . . 8
โข (๐ฆ = (๐นโ๐) โ (โ๐ง โ ran ๐นโ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค โ โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค)) |
83 | 82 | ralrn 7038 |
. . . . . . 7
โข (๐น Fn ๐ โ (โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค โ โ๐ โ ๐ โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค)) |
84 | 71, 83 | syl 17 |
. . . . . 6
โข (๐ โ (โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค โ โ๐ โ ๐ โ๐ง โ ran ๐นโ*๐คโจ(๐นโ๐), ๐งโฉ โ ๐ค)) |
85 | 78, 84 | mpbird 256 |
. . . . 5
โข (๐ โ โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค) |
86 | | breq1 5108 |
. . . . . . 7
โข (๐ฅ = โจ๐ฆ, ๐งโฉ โ (๐ฅ โ ๐ค โ โจ๐ฆ, ๐งโฉ โ ๐ค)) |
87 | 86 | mobidv 2547 |
. . . . . 6
โข (๐ฅ = โจ๐ฆ, ๐งโฉ โ (โ*๐ค ๐ฅ โ ๐ค โ โ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค)) |
88 | 87 | ralxp 5797 |
. . . . 5
โข
(โ๐ฅ โ
(ran ๐น ร ran ๐น)โ*๐ค ๐ฅ โ ๐ค โ โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโ*๐คโจ๐ฆ, ๐งโฉ โ ๐ค) |
89 | 85, 88 | sylibr 233 |
. . . 4
โข (๐ โ โ๐ฅ โ (ran ๐น ร ran ๐น)โ*๐ค ๐ฅ โ ๐ค) |
90 | | ssralv 4010 |
. . . 4
โข (dom
โ
โ (ran ๐น ร ran
๐น) โ (โ๐ฅ โ (ran ๐น ร ran ๐น)โ*๐ค ๐ฅ โ ๐ค โ โ๐ฅ โ dom โ โ*๐ค ๐ฅ โ ๐ค)) |
91 | 38, 89, 90 | sylc 65 |
. . 3
โข (๐ โ โ๐ฅ โ dom โ โ*๐ค ๐ฅ โ ๐ค) |
92 | | dffun7 6528 |
. . 3
โข (Fun
โ
โ (Rel โ โง โ๐ฅ โ dom โ โ*๐ค ๐ฅ โ ๐ค)) |
93 | 12, 91, 92 | sylanbrc 583 |
. 2
โข (๐ โ Fun โ ) |
94 | | eqimss2 4001 |
. . . . . . . . . . 11
โข ( โ =
โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ ) |
95 | 10, 94 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ ) |
96 | | iunss 5005 |
. . . . . . . . . 10
โข (โช ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ โ
โ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ ) |
97 | 95, 96 | sylib 217 |
. . . . . . . . 9
โข (๐ โ โ๐ โ ๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ ) |
98 | | iunss 5005 |
. . . . . . . . . . 11
โข (โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ โ
โ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ ) |
99 | | opex 5421 |
. . . . . . . . . . . . . 14
โข
โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ V |
100 | 99 | snss 4746 |
. . . . . . . . . . . . 13
โข
(โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ โ โ
{โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ ) |
101 | 1, 2 | opeldm 5863 |
. . . . . . . . . . . . 13
โข
(โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ โ โ โ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ ) |
102 | 100, 101 | sylbir 234 |
. . . . . . . . . . . 12
โข
({โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ โ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ ) |
103 | 102 | ralimi 3086 |
. . . . . . . . . . 11
โข
(โ๐ โ
๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ โ
โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ ) |
104 | 98, 103 | sylbi 216 |
. . . . . . . . . 10
โข (โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ โ
โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ ) |
105 | 104 | ralimi 3086 |
. . . . . . . . 9
โข
(โ๐ โ
๐ โช ๐ โ ๐ {โจโจ(๐นโ๐), (๐นโ๐)โฉ, (๐นโ(๐ ยท ๐))โฉ} โ โ โ
โ๐ โ ๐ โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ ) |
106 | 97, 105 | syl 17 |
. . . . . . . 8
โข (๐ โ โ๐ โ ๐ โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ ) |
107 | | opeq2 4831 |
. . . . . . . . . . . 12
โข (๐ง = (๐นโ๐) โ โจ(๐นโ๐), ๐งโฉ = โจ(๐นโ๐), (๐นโ๐)โฉ) |
108 | 107 | eleq1d 2822 |
. . . . . . . . . . 11
โข (๐ง = (๐นโ๐) โ (โจ(๐นโ๐), ๐งโฉ โ dom โ โ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ )) |
109 | 108 | ralrn 7038 |
. . . . . . . . . 10
โข (๐น Fn ๐ โ (โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ โ
โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ )) |
110 | 71, 109 | syl 17 |
. . . . . . . . 9
โข (๐ โ (โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ โ
โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ )) |
111 | 110 | ralbidv 3174 |
. . . . . . . 8
โข (๐ โ (โ๐ โ ๐ โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ โ
โ๐ โ ๐ โ๐ โ ๐ โจ(๐นโ๐), (๐นโ๐)โฉ โ dom โ )) |
112 | 106, 111 | mpbird 256 |
. . . . . . 7
โข (๐ โ โ๐ โ ๐ โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ ) |
113 | | opeq1 4830 |
. . . . . . . . . . 11
โข (๐ฆ = (๐นโ๐) โ โจ๐ฆ, ๐งโฉ = โจ(๐นโ๐), ๐งโฉ) |
114 | 113 | eleq1d 2822 |
. . . . . . . . . 10
โข (๐ฆ = (๐นโ๐) โ (โจ๐ฆ, ๐งโฉ โ dom โ โ โจ(๐นโ๐), ๐งโฉ โ dom โ )) |
115 | 114 | ralbidv 3174 |
. . . . . . . . 9
โข (๐ฆ = (๐นโ๐) โ (โ๐ง โ ran ๐นโจ๐ฆ, ๐งโฉ โ dom โ โ
โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ )) |
116 | 115 | ralrn 7038 |
. . . . . . . 8
โข (๐น Fn ๐ โ (โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโจ๐ฆ, ๐งโฉ โ dom โ โ
โ๐ โ ๐ โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ )) |
117 | 71, 116 | syl 17 |
. . . . . . 7
โข (๐ โ (โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโจ๐ฆ, ๐งโฉ โ dom โ โ
โ๐ โ ๐ โ๐ง โ ran ๐นโจ(๐นโ๐), ๐งโฉ โ dom โ )) |
118 | 112, 117 | mpbird 256 |
. . . . . 6
โข (๐ โ โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโจ๐ฆ, ๐งโฉ โ dom โ ) |
119 | | eleq1 2825 |
. . . . . . 7
โข (๐ฅ = โจ๐ฆ, ๐งโฉ โ (๐ฅ โ dom โ โ โจ๐ฆ, ๐งโฉ โ dom โ )) |
120 | 119 | ralxp 5797 |
. . . . . 6
โข
(โ๐ฅ โ
(ran ๐น ร ran ๐น)๐ฅ โ dom โ โ
โ๐ฆ โ ran ๐นโ๐ง โ ran ๐นโจ๐ฆ, ๐งโฉ โ dom โ ) |
121 | 118, 120 | sylibr 233 |
. . . . 5
โข (๐ โ โ๐ฅ โ (ran ๐น ร ran ๐น)๐ฅ โ dom โ ) |
122 | | dfss3 3932 |
. . . . 5
โข ((ran
๐น ร ran ๐น) โ dom โ โ
โ๐ฅ โ (ran ๐น ร ran ๐น)๐ฅ โ dom โ ) |
123 | 121, 122 | sylibr 233 |
. . . 4
โข (๐ โ (ran ๐น ร ran ๐น) โ dom โ ) |
124 | 37, 123 | eqsstrrd 3983 |
. . 3
โข (๐ โ (๐ต ร ๐ต) โ dom โ ) |
125 | 34, 124 | eqssd 3961 |
. 2
โข (๐ โ dom โ = (๐ต ร ๐ต)) |
126 | | df-fn 6499 |
. 2
โข ( โ Fn
(๐ต ร ๐ต) โ (Fun โ โง dom โ =
(๐ต ร ๐ต))) |
127 | 93, 125, 126 | sylanbrc 583 |
1
โข (๐ โ โ Fn (๐ต ร ๐ต)) |