Metamath Proof Explorer

Theorem imasaddflem

Description: The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasaddf.f 
|- ( ph -> F : V -onto-> B )
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 ) ) ) )
imasaddflem.a 
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
imasaddflem.c 
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
Assertion imasaddflem 
|- ( ph -> .xb : ( B X. B ) --> B )

Proof

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 ffvelcdm 
 |-  ( ( F : V --> B /\ p e. V ) -> ( F ` p ) e. B )
9 ffvelcdm 
 |-  ( ( 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 ffvelcdm 
 |-  ( ( 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 )