Step |
Hyp |
Ref |
Expression |
1 |
|
imasaddf.f |
|- ( ph -> F : V -onto-> B ) |
2 |
|
imasaddf.e |
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) ) |
3 |
|
imasaddflem.a |
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) |
4 |
|
imasaddflem.c |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V ) |
5 |
1 2 3
|
imasaddfnlem |
|- ( ph -> .xb Fn ( B X. B ) ) |
6 |
|
fof |
|- ( F : V -onto-> B -> F : V --> B ) |
7 |
1 6
|
syl |
|- ( ph -> F : V --> B ) |
8 |
|
ffvelrn |
|- ( ( F : V --> B /\ p e. V ) -> ( F ` p ) e. B ) |
9 |
|
ffvelrn |
|- ( ( F : V --> B /\ q e. V ) -> ( F ` q ) e. B ) |
10 |
8 9
|
anim12dan |
|- ( ( F : V --> B /\ ( p e. V /\ q e. V ) ) -> ( ( F ` p ) e. B /\ ( F ` q ) e. B ) ) |
11 |
|
opelxpi |
|- ( ( ( F ` p ) e. B /\ ( F ` q ) e. B ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) ) |
12 |
10 11
|
syl |
|- ( ( F : V --> B /\ ( p e. V /\ q e. V ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) ) |
13 |
7 12
|
sylan |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. ( F ` p ) , ( F ` q ) >. e. ( B X. B ) ) |
14 |
|
ffvelrn |
|- ( ( F : V --> B /\ ( p .x. q ) e. V ) -> ( F ` ( p .x. q ) ) e. B ) |
15 |
7 4 14
|
syl2an2r |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( F ` ( p .x. q ) ) e. B ) |
16 |
13 15
|
opelxpd |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. e. ( ( B X. B ) X. B ) ) |
17 |
16
|
snssd |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. B ) ) |
18 |
17
|
anassrs |
|- ( ( ( ph /\ p e. V ) /\ q e. V ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. B ) ) |
19 |
18
|
iunssd |
|- ( ( ph /\ p e. V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. B ) ) |
20 |
19
|
iunssd |
|- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } C_ ( ( B X. B ) X. B ) ) |
21 |
3 20
|
eqsstrd |
|- ( ph -> .xb C_ ( ( B X. B ) X. B ) ) |
22 |
|
dff2 |
|- ( .xb : ( B X. B ) --> B <-> ( .xb Fn ( B X. B ) /\ .xb C_ ( ( B X. B ) X. B ) ) ) |
23 |
5 21 22
|
sylanbrc |
|- ( ph -> .xb : ( B X. B ) --> B ) |