Step |
Hyp |
Ref |
Expression |
1 |
|
imasvscaf.u |
โข ( ๐ โ ๐ = ( ๐น โs ๐
) ) |
2 |
|
imasvscaf.v |
โข ( ๐ โ ๐ = ( Base โ ๐
) ) |
3 |
|
imasvscaf.f |
โข ( ๐ โ ๐น : ๐ โontoโ ๐ต ) |
4 |
|
imasvscaf.r |
โข ( ๐ โ ๐
โ ๐ ) |
5 |
|
imasvscaf.g |
โข ๐บ = ( Scalar โ ๐
) |
6 |
|
imasvscaf.k |
โข ๐พ = ( Base โ ๐บ ) |
7 |
|
imasvscaf.q |
โข ยท = ( ยท๐ โ ๐
) |
8 |
|
imasvscaf.s |
โข โ = ( ยท๐ โ ๐ ) |
9 |
|
imasvscaf.e |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ( ๐น โ ๐ ) = ( ๐น โ ๐ ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
10 |
|
eqid |
โข ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) = ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) |
11 |
|
fvex |
โข ( ๐น โ ( ๐ ยท ๐ ) ) โ V |
12 |
10 11
|
fnmpoi |
โข ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) Fn ( ๐พ ร { ( ๐น โ ๐ ) } ) |
13 |
|
fnrel |
โข ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) Fn ( ๐พ ร { ( ๐น โ ๐ ) } ) โ Rel ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
14 |
12 13
|
ax-mp |
โข Rel ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) |
15 |
14
|
rgenw |
โข โ ๐ โ ๐ Rel ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) |
16 |
|
reliun |
โข ( Rel โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ๐ โ ๐ Rel ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
17 |
15 16
|
mpbir |
โข Rel โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) |
18 |
1 2 3 4 5 6 7 8
|
imasvsca |
โข ( ๐ โ โ = โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
19 |
18
|
releqd |
โข ( ๐ โ ( Rel โ โ Rel โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) ) |
20 |
17 19
|
mpbiri |
โข ( ๐ โ Rel โ ) |
21 |
|
dffn2 |
โข ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) Fn ( ๐พ ร { ( ๐น โ ๐ ) } ) โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) : ( ๐พ ร { ( ๐น โ ๐ ) } ) โถ V ) |
22 |
12 21
|
mpbi |
โข ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) : ( ๐พ ร { ( ๐น โ ๐ ) } ) โถ V |
23 |
|
fssxp |
โข ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) : ( ๐พ ร { ( ๐น โ ๐ ) } ) โถ V โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร { ( ๐น โ ๐ ) } ) ร V ) ) |
24 |
22 23
|
ax-mp |
โข ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร { ( ๐น โ ๐ ) } ) ร V ) |
25 |
|
fof |
โข ( ๐น : ๐ โontoโ ๐ต โ ๐น : ๐ โถ ๐ต ) |
26 |
3 25
|
syl |
โข ( ๐ โ ๐น : ๐ โถ ๐ต ) |
27 |
26
|
ffvelrnda |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ๐น โ ๐ ) โ ๐ต ) |
28 |
27
|
snssd |
โข ( ( ๐ โง ๐ โ ๐ ) โ { ( ๐น โ ๐ ) } โ ๐ต ) |
29 |
|
xpss2 |
โข ( { ( ๐น โ ๐ ) } โ ๐ต โ ( ๐พ ร { ( ๐น โ ๐ ) } ) โ ( ๐พ ร ๐ต ) ) |
30 |
|
xpss1 |
โข ( ( ๐พ ร { ( ๐น โ ๐ ) } ) โ ( ๐พ ร ๐ต ) โ ( ( ๐พ ร { ( ๐น โ ๐ ) } ) ร V ) โ ( ( ๐พ ร ๐ต ) ร V ) ) |
31 |
28 29 30
|
3syl |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ( ๐พ ร { ( ๐น โ ๐ ) } ) ร V ) โ ( ( ๐พ ร ๐ต ) ร V ) ) |
32 |
24 31
|
sstrid |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร ๐ต ) ร V ) ) |
33 |
32
|
ralrimiva |
โข ( ๐ โ โ ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร ๐ต ) ร V ) ) |
34 |
|
iunss |
โข ( โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร ๐ต ) ร V ) โ โ ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร ๐ต ) ร V ) ) |
35 |
33 34
|
sylibr |
โข ( ๐ โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐พ ร ๐ต ) ร V ) ) |
36 |
18 35
|
eqsstrd |
โข ( ๐ โ โ โ ( ( ๐พ ร ๐ต ) ร V ) ) |
37 |
|
dmss |
โข ( โ โ ( ( ๐พ ร ๐ต ) ร V ) โ dom โ โ dom ( ( ๐พ ร ๐ต ) ร V ) ) |
38 |
36 37
|
syl |
โข ( ๐ โ dom โ โ dom ( ( ๐พ ร ๐ต ) ร V ) ) |
39 |
|
vn0 |
โข V โ โ
|
40 |
|
dmxp |
โข ( V โ โ
โ dom ( ( ๐พ ร ๐ต ) ร V ) = ( ๐พ ร ๐ต ) ) |
41 |
39 40
|
ax-mp |
โข dom ( ( ๐พ ร ๐ต ) ร V ) = ( ๐พ ร ๐ต ) |
42 |
38 41
|
sseqtrdi |
โข ( ๐ โ dom โ โ ( ๐พ ร ๐ต ) ) |
43 |
|
forn |
โข ( ๐น : ๐ โontoโ ๐ต โ ran ๐น = ๐ต ) |
44 |
3 43
|
syl |
โข ( ๐ โ ran ๐น = ๐ต ) |
45 |
44
|
xpeq2d |
โข ( ๐ โ ( ๐พ ร ran ๐น ) = ( ๐พ ร ๐ต ) ) |
46 |
42 45
|
sseqtrrd |
โข ( ๐ โ dom โ โ ( ๐พ ร ran ๐น ) ) |
47 |
|
df-br |
โข ( โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค โ โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โ ) |
48 |
18
|
eleq2d |
โข ( ๐ โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โ โ โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) ) |
49 |
48
|
adantr |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โ โ โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) ) |
50 |
|
eliun |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ๐ โ ๐ โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
51 |
|
df-3an |
โข ( ( ๐ โ ๐พ โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ โ ๐พ โง ๐ โ ๐ ) โง ๐ โ ๐ ) ) |
52 |
10
|
mpofun |
โข Fun ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) |
53 |
|
funopfv |
โข ( Fun ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ ) = ๐ค ) ) |
54 |
52 53
|
ax-mp |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ ) = ๐ค ) |
55 |
|
df-ov |
โข ( ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ( ๐น โ ๐ ) ) = ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ ) |
56 |
|
opex |
โข โจ ๐ , ( ๐น โ ๐ ) โฉ โ V |
57 |
|
vex |
โข ๐ค โ V |
58 |
56 57
|
opeldm |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
59 |
10 11
|
dmmpo |
โข dom ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) = ( ๐พ ร { ( ๐น โ ๐ ) } ) |
60 |
58 59
|
eleqtrdi |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ ( ๐พ ร { ( ๐น โ ๐ ) } ) ) |
61 |
|
opelxp |
โข ( โจ ๐ , ( ๐น โ ๐ ) โฉ โ ( ๐พ ร { ( ๐น โ ๐ ) } ) โ ( ๐ โ ๐พ โง ( ๐น โ ๐ ) โ { ( ๐น โ ๐ ) } ) ) |
62 |
60 61
|
sylib |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ๐ โ ๐พ โง ( ๐น โ ๐ ) โ { ( ๐น โ ๐ ) } ) ) |
63 |
|
fvoveq1 |
โข ( ๐ง = ๐ โ ( ๐น โ ( ๐ง ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
64 |
|
eqidd |
โข ( ๐ฆ = ( ๐น โ ๐ ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
65 |
|
fvoveq1 |
โข ( ๐ = ๐ง โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ง ยท ๐ ) ) ) |
66 |
|
eqidd |
โข ( ๐ฅ = ๐ฆ โ ( ๐น โ ( ๐ง ยท ๐ ) ) = ( ๐น โ ( ๐ง ยท ๐ ) ) ) |
67 |
65 66
|
cbvmpov |
โข ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) = ( ๐ง โ ๐พ , ๐ฆ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ง ยท ๐ ) ) ) |
68 |
63 64 67 11
|
ovmpo |
โข ( ( ๐ โ ๐พ โง ( ๐น โ ๐ ) โ { ( ๐น โ ๐ ) } ) โ ( ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ( ๐น โ ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
69 |
62 68
|
syl |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ( ๐น โ ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
70 |
55 69
|
eqtr3id |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
71 |
54 70
|
eqtr3d |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
72 |
71
|
adantl |
โข ( ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ โง ๐ โ ๐ ) ) โง โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
73 |
|
elsni |
โข ( ( ๐น โ ๐ ) โ { ( ๐น โ ๐ ) } โ ( ๐น โ ๐ ) = ( ๐น โ ๐ ) ) |
74 |
62 73
|
simpl2im |
โข ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ( ๐น โ ๐ ) = ( ๐น โ ๐ ) ) |
75 |
9 74
|
impel |
โข ( ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ โง ๐ โ ๐ ) ) โง โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
76 |
72 75
|
eqtr4d |
โข ( ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ โง ๐ โ ๐ ) ) โง โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
77 |
76
|
ex |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
78 |
51 77
|
sylan2br |
โข ( ( ๐ โง ( ( ๐ โ ๐พ โง ๐ โ ๐ ) โง ๐ โ ๐ ) ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
79 |
78
|
anassrs |
โข ( ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โง ๐ โ ๐ ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
80 |
79
|
rexlimdva |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( โ ๐ โ ๐ โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
81 |
50 80
|
syl5bi |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
82 |
49 81
|
sylbid |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( โจ โจ ๐ , ( ๐น โ ๐ ) โฉ , ๐ค โฉ โ โ โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
83 |
47 82
|
syl5bi |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
84 |
83
|
alrimiv |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ โ ๐ค ( โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
85 |
|
mo2icl |
โข ( โ ๐ค ( โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค โ ๐ค = ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) |
86 |
84 85
|
syl |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) |
87 |
86
|
ralrimivva |
โข ( ๐ โ โ ๐ โ ๐พ โ ๐ โ ๐ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) |
88 |
|
fofn |
โข ( ๐น : ๐ โontoโ ๐ต โ ๐น Fn ๐ ) |
89 |
|
opeq2 |
โข ( ๐ฆ = ( ๐น โ ๐ ) โ โจ ๐ , ๐ฆ โฉ = โจ ๐ , ( ๐น โ ๐ ) โฉ ) |
90 |
89
|
breq1d |
โข ( ๐ฆ = ( ๐น โ ๐ ) โ ( โจ ๐ , ๐ฆ โฉ โ ๐ค โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) ) |
91 |
90
|
mobidv |
โข ( ๐ฆ = ( ๐น โ ๐ ) โ ( โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค โ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) ) |
92 |
91
|
ralrn |
โข ( ๐น Fn ๐ โ ( โ ๐ฆ โ ran ๐น โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค โ โ ๐ โ ๐ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) ) |
93 |
3 88 92
|
3syl |
โข ( ๐ โ ( โ ๐ฆ โ ran ๐น โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค โ โ ๐ โ ๐ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) ) |
94 |
93
|
ralbidv |
โข ( ๐ โ ( โ ๐ โ ๐พ โ ๐ฆ โ ran ๐น โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค โ โ ๐ โ ๐พ โ ๐ โ ๐ โ* ๐ค โจ ๐ , ( ๐น โ ๐ ) โฉ โ ๐ค ) ) |
95 |
87 94
|
mpbird |
โข ( ๐ โ โ ๐ โ ๐พ โ ๐ฆ โ ran ๐น โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค ) |
96 |
|
breq1 |
โข ( ๐ฅ = โจ ๐ , ๐ฆ โฉ โ ( ๐ฅ โ ๐ค โ โจ ๐ , ๐ฆ โฉ โ ๐ค ) ) |
97 |
96
|
mobidv |
โข ( ๐ฅ = โจ ๐ , ๐ฆ โฉ โ ( โ* ๐ค ๐ฅ โ ๐ค โ โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค ) ) |
98 |
97
|
ralxp |
โข ( โ ๐ฅ โ ( ๐พ ร ran ๐น ) โ* ๐ค ๐ฅ โ ๐ค โ โ ๐ โ ๐พ โ ๐ฆ โ ran ๐น โ* ๐ค โจ ๐ , ๐ฆ โฉ โ ๐ค ) |
99 |
95 98
|
sylibr |
โข ( ๐ โ โ ๐ฅ โ ( ๐พ ร ran ๐น ) โ* ๐ค ๐ฅ โ ๐ค ) |
100 |
|
ssralv |
โข ( dom โ โ ( ๐พ ร ran ๐น ) โ ( โ ๐ฅ โ ( ๐พ ร ran ๐น ) โ* ๐ค ๐ฅ โ ๐ค โ โ ๐ฅ โ dom โ โ* ๐ค ๐ฅ โ ๐ค ) ) |
101 |
46 99 100
|
sylc |
โข ( ๐ โ โ ๐ฅ โ dom โ โ* ๐ค ๐ฅ โ ๐ค ) |
102 |
|
dffun7 |
โข ( Fun โ โ ( Rel โ โง โ ๐ฅ โ dom โ โ* ๐ค ๐ฅ โ ๐ค ) ) |
103 |
20 101 102
|
sylanbrc |
โข ( ๐ โ Fun โ ) |
104 |
|
eqimss2 |
โข ( โ = โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ) |
105 |
18 104
|
syl |
โข ( ๐ โ โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ) |
106 |
|
iunss |
โข ( โช ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ โ โ ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ) |
107 |
105 106
|
sylib |
โข ( ๐ โ โ ๐ โ ๐ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ) |
108 |
107
|
r19.21bi |
โข ( ( ๐ โง ๐ โ ๐ ) โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ) |
109 |
108
|
adantrl |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ ) |
110 |
|
dmss |
โข ( ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ โ โ dom ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ dom โ ) |
111 |
109 110
|
syl |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ dom ( ๐ โ ๐พ , ๐ฅ โ { ( ๐น โ ๐ ) } โฆ ( ๐น โ ( ๐ ยท ๐ ) ) ) โ dom โ ) |
112 |
59 111
|
eqsstrrid |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ( ๐พ ร { ( ๐น โ ๐ ) } ) โ dom โ ) |
113 |
|
simprl |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ ๐ โ ๐พ ) |
114 |
|
fvex |
โข ( ๐น โ ๐ ) โ V |
115 |
114
|
snid |
โข ( ๐น โ ๐ ) โ { ( ๐น โ ๐ ) } |
116 |
|
opelxpi |
โข ( ( ๐ โ ๐พ โง ( ๐น โ ๐ ) โ { ( ๐น โ ๐ ) } ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ ( ๐พ ร { ( ๐น โ ๐ ) } ) ) |
117 |
113 115 116
|
sylancl |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ ( ๐พ ร { ( ๐น โ ๐ ) } ) ) |
118 |
112 117
|
sseldd |
โข ( ( ๐ โง ( ๐ โ ๐พ โง ๐ โ ๐ ) ) โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom โ ) |
119 |
118
|
ralrimivva |
โข ( ๐ โ โ ๐ โ ๐พ โ ๐ โ ๐ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom โ ) |
120 |
|
opeq2 |
โข ( ๐ฆ = ( ๐น โ ๐ ) โ โจ ๐ , ๐ฆ โฉ = โจ ๐ , ( ๐น โ ๐ ) โฉ ) |
121 |
120
|
eleq1d |
โข ( ๐ฆ = ( ๐น โ ๐ ) โ ( โจ ๐ , ๐ฆ โฉ โ dom โ โ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom โ ) ) |
122 |
121
|
ralrn |
โข ( ๐น Fn ๐ โ ( โ ๐ฆ โ ran ๐น โจ ๐ , ๐ฆ โฉ โ dom โ โ โ ๐ โ ๐ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom โ ) ) |
123 |
3 88 122
|
3syl |
โข ( ๐ โ ( โ ๐ฆ โ ran ๐น โจ ๐ , ๐ฆ โฉ โ dom โ โ โ ๐ โ ๐ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom โ ) ) |
124 |
123
|
ralbidv |
โข ( ๐ โ ( โ ๐ โ ๐พ โ ๐ฆ โ ran ๐น โจ ๐ , ๐ฆ โฉ โ dom โ โ โ ๐ โ ๐พ โ ๐ โ ๐ โจ ๐ , ( ๐น โ ๐ ) โฉ โ dom โ ) ) |
125 |
119 124
|
mpbird |
โข ( ๐ โ โ ๐ โ ๐พ โ ๐ฆ โ ran ๐น โจ ๐ , ๐ฆ โฉ โ dom โ ) |
126 |
|
eleq1 |
โข ( ๐ฅ = โจ ๐ , ๐ฆ โฉ โ ( ๐ฅ โ dom โ โ โจ ๐ , ๐ฆ โฉ โ dom โ ) ) |
127 |
126
|
ralxp |
โข ( โ ๐ฅ โ ( ๐พ ร ran ๐น ) ๐ฅ โ dom โ โ โ ๐ โ ๐พ โ ๐ฆ โ ran ๐น โจ ๐ , ๐ฆ โฉ โ dom โ ) |
128 |
125 127
|
sylibr |
โข ( ๐ โ โ ๐ฅ โ ( ๐พ ร ran ๐น ) ๐ฅ โ dom โ ) |
129 |
|
dfss3 |
โข ( ( ๐พ ร ran ๐น ) โ dom โ โ โ ๐ฅ โ ( ๐พ ร ran ๐น ) ๐ฅ โ dom โ ) |
130 |
128 129
|
sylibr |
โข ( ๐ โ ( ๐พ ร ran ๐น ) โ dom โ ) |
131 |
45 130
|
eqsstrrd |
โข ( ๐ โ ( ๐พ ร ๐ต ) โ dom โ ) |
132 |
42 131
|
eqssd |
โข ( ๐ โ dom โ = ( ๐พ ร ๐ต ) ) |
133 |
|
df-fn |
โข ( โ Fn ( ๐พ ร ๐ต ) โ ( Fun โ โง dom โ = ( ๐พ ร ๐ต ) ) ) |
134 |
103 132 133
|
sylanbrc |
โข ( ๐ โ โ Fn ( ๐พ ร ๐ต ) ) |