ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasaddvallemg GIF version

Theorem imasaddvallemg 12765
Description: The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.)
Hypotheses
Ref Expression
imasaddf.f (๐œ‘ โ†’ ๐น:๐‘‰โ€“ontoโ†’๐ต)
imasaddf.e ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž)) โ†’ (๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž))))
imasaddflem.a (๐œ‘ โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
imasaddfnlemg.v (๐œ‘ โ†’ ๐‘‰ โˆˆ ๐‘Š)
imasaddfnlemg.x (๐œ‘ โ†’ ยท โˆˆ ๐ถ)
Assertion
Ref Expression
imasaddvallemg ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
Distinct variable groups:   ๐‘ž,๐‘,๐ต   ๐‘Ž,๐‘,๐‘,๐‘ž,๐‘‰   ยท ,๐‘,๐‘ž   ๐‘‹,๐‘   ๐น,๐‘Ž,๐‘,๐‘,๐‘ž   ๐œ‘,๐‘Ž,๐‘,๐‘,๐‘ž   โˆ™ ,๐‘Ž,๐‘,๐‘,๐‘ž   ๐‘Œ,๐‘,๐‘ž
Allowed substitution hints:   ๐ต(๐‘Ž,๐‘)   ๐ถ(๐‘ž,๐‘,๐‘Ž,๐‘)   ยท (๐‘Ž,๐‘)   ๐‘Š(๐‘ž,๐‘,๐‘Ž,๐‘)   ๐‘‹(๐‘ž,๐‘Ž,๐‘)   ๐‘Œ(๐‘Ž,๐‘)

Proof of Theorem imasaddvallemg
StepHypRef Expression
1 df-ov 5895 . 2 ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ)
2 imasaddf.f . . . . . 6 (๐œ‘ โ†’ ๐น:๐‘‰โ€“ontoโ†’๐ต)
3 imasaddf.e . . . . . 6 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž)) โ†’ (๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž))))
4 imasaddflem.a . . . . . 6 (๐œ‘ โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
5 imasaddfnlemg.v . . . . . 6 (๐œ‘ โ†’ ๐‘‰ โˆˆ ๐‘Š)
6 imasaddfnlemg.x . . . . . 6 (๐œ‘ โ†’ ยท โˆˆ ๐ถ)
72, 3, 4, 5, 6imasaddfnlemg 12764 . . . . 5 (๐œ‘ โ†’ โˆ™ Fn (๐ต ร— ๐ต))
8 fnfun 5329 . . . . 5 ( โˆ™ Fn (๐ต ร— ๐ต) โ†’ Fun โˆ™ )
97, 8syl 14 . . . 4 (๐œ‘ โ†’ Fun โˆ™ )
1093ad2ant1 1020 . . 3 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ Fun โˆ™ )
11 fveq2 5531 . . . . . . . . . . 11 (๐‘ = ๐‘‹ โ†’ (๐นโ€˜๐‘) = (๐นโ€˜๐‘‹))
1211opeq1d 3799 . . . . . . . . . 10 (๐‘ = ๐‘‹ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ = โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ)
13 fvoveq1 5915 . . . . . . . . . 10 (๐‘ = ๐‘‹ โ†’ (๐นโ€˜(๐‘ ยท ๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
1412, 13opeq12d 3801 . . . . . . . . 9 (๐‘ = ๐‘‹ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ = โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ)
1514sneqd 3620 . . . . . . . 8 (๐‘ = ๐‘‹ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} = {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ})
1615ssiun2s 3945 . . . . . . 7 (๐‘‹ โˆˆ ๐‘‰ โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
17163ad2ant2 1021 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
18 fveq2 5531 . . . . . . . . . . . . 13 (๐‘ž = ๐‘Œ โ†’ (๐นโ€˜๐‘ž) = (๐นโ€˜๐‘Œ))
1918opeq2d 3800 . . . . . . . . . . . 12 (๐‘ž = ๐‘Œ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ)
20 oveq2 5900 . . . . . . . . . . . . 13 (๐‘ž = ๐‘Œ โ†’ (๐‘ ยท ๐‘ž) = (๐‘ ยท ๐‘Œ))
2120fveq2d 5535 . . . . . . . . . . . 12 (๐‘ž = ๐‘Œ โ†’ (๐นโ€˜(๐‘ ยท ๐‘ž)) = (๐นโ€˜(๐‘ ยท ๐‘Œ)))
2219, 21opeq12d 3801 . . . . . . . . . . 11 (๐‘ž = ๐‘Œ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ)
2322sneqd 3620 . . . . . . . . . 10 (๐‘ž = ๐‘Œ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} = {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
2423ssiun2s 3945 . . . . . . . . 9 (๐‘Œ โˆˆ ๐‘‰ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2524ralrimivw 2564 . . . . . . . 8 (๐‘Œ โˆˆ ๐‘‰ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
26 ss2iun 3916 . . . . . . . 8 (โˆ€๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2725, 26syl 14 . . . . . . 7 (๐‘Œ โˆˆ ๐‘‰ โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
28273ad2ant3 1022 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2917, 28sstrd 3180 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
3043ad2ant1 1020 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
3129, 30sseqtrrd 3209 . . . 4 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ )
32 fof 5454 . . . . . . . . . . 11 (๐น:๐‘‰โ€“ontoโ†’๐ต โ†’ ๐น:๐‘‰โŸถ๐ต)
332, 32syl 14 . . . . . . . . . 10 (๐œ‘ โ†’ ๐น:๐‘‰โŸถ๐ต)
34333ad2ant1 1020 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐น:๐‘‰โŸถ๐ต)
3553ad2ant1 1020 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐‘‰ โˆˆ ๐‘Š)
3634, 35fexd 5763 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐น โˆˆ V)
37 simp2 1000 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐‘‹ โˆˆ ๐‘‰)
38 fvexg 5550 . . . . . . . 8 ((๐น โˆˆ V โˆง ๐‘‹ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘‹) โˆˆ V)
3936, 37, 38syl2anc 411 . . . . . . 7 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘‹) โˆˆ V)
40 simp3 1001 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐‘Œ โˆˆ ๐‘‰)
41 fvexg 5550 . . . . . . . 8 ((๐น โˆˆ V โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘Œ) โˆˆ V)
4236, 40, 41syl2anc 411 . . . . . . 7 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘Œ) โˆˆ V)
43 opexg 4243 . . . . . . 7 (((๐นโ€˜๐‘‹) โˆˆ V โˆง (๐นโ€˜๐‘Œ) โˆˆ V) โ†’ โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ โˆˆ V)
4439, 42, 43syl2anc 411 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ โˆˆ V)
4563ad2ant1 1020 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ยท โˆˆ ๐ถ)
46 ovexg 5926 . . . . . . . 8 ((๐‘‹ โˆˆ ๐‘‰ โˆง ยท โˆˆ ๐ถ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐‘‹ ยท ๐‘Œ) โˆˆ V)
4737, 45, 40, 46syl3anc 1249 . . . . . . 7 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐‘‹ ยท ๐‘Œ) โˆˆ V)
48 fvexg 5550 . . . . . . 7 ((๐น โˆˆ V โˆง (๐‘‹ ยท ๐‘Œ) โˆˆ V) โ†’ (๐นโ€˜(๐‘‹ ยท ๐‘Œ)) โˆˆ V)
4936, 47, 48syl2anc 411 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜(๐‘‹ ยท ๐‘Œ)) โˆˆ V)
50 opexg 4243 . . . . . 6 ((โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ โˆˆ V โˆง (๐นโ€˜(๐‘‹ ยท ๐‘Œ)) โˆˆ V) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V)
5144, 49, 50syl2anc 411 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V)
52 snssg 3741 . . . . 5 (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ ))
5351, 52syl 14 . . . 4 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ ))
5431, 53mpbird 167 . . 3 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ )
55 funopfv 5572 . . 3 (Fun โˆ™ โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†’ ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ))))
5610, 54, 55sylc 62 . 2 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
571, 56eqtrid 2234 1 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 980   = wceq 1364   โˆˆ wcel 2160  โˆ€wral 2468  Vcvv 2752   โІ wss 3144  {csn 3607  โŸจcop 3610  โˆช ciun 3901   ร— cxp 4639  Fun wfun 5226   Fn wfn 5227  โŸถwf 5228  โ€“ontoโ†’wfo 5230  โ€˜cfv 5232  (class class class)co 5892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5234  df-fn 5235  df-f 5236  df-f1 5237  df-fo 5238  df-f1o 5239  df-fv 5240  df-ov 5895
This theorem is referenced by:  imasaddval  12768  imasmulval  12771  qusaddvallemg  12782
  Copyright terms: Public domain W3C validator