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

Theorem imasaddvallemg 12753
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 5891 . 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 12752 . . . . 5 (๐œ‘ โ†’ โˆ™ Fn (๐ต ร— ๐ต))
8 fnfun 5325 . . . . 5 ( โˆ™ Fn (๐ต ร— ๐ต) โ†’ Fun โˆ™ )
97, 8syl 14 . . . 4 (๐œ‘ โ†’ Fun โˆ™ )
1093ad2ant1 1019 . . 3 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ Fun โˆ™ )
11 fveq2 5527 . . . . . . . . . . 11 (๐‘ = ๐‘‹ โ†’ (๐นโ€˜๐‘) = (๐นโ€˜๐‘‹))
1211opeq1d 3796 . . . . . . . . . 10 (๐‘ = ๐‘‹ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ = โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ)
13 fvoveq1 5911 . . . . . . . . . 10 (๐‘ = ๐‘‹ โ†’ (๐นโ€˜(๐‘ ยท ๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
1412, 13opeq12d 3798 . . . . . . . . 9 (๐‘ = ๐‘‹ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ = โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ)
1514sneqd 3617 . . . . . . . 8 (๐‘ = ๐‘‹ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} = {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ})
1615ssiun2s 3942 . . . . . . 7 (๐‘‹ โˆˆ ๐‘‰ โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
17163ad2ant2 1020 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
18 fveq2 5527 . . . . . . . . . . . . 13 (๐‘ž = ๐‘Œ โ†’ (๐นโ€˜๐‘ž) = (๐นโ€˜๐‘Œ))
1918opeq2d 3797 . . . . . . . . . . . 12 (๐‘ž = ๐‘Œ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ)
20 oveq2 5896 . . . . . . . . . . . . 13 (๐‘ž = ๐‘Œ โ†’ (๐‘ ยท ๐‘ž) = (๐‘ ยท ๐‘Œ))
2120fveq2d 5531 . . . . . . . . . . . 12 (๐‘ž = ๐‘Œ โ†’ (๐นโ€˜(๐‘ ยท ๐‘ž)) = (๐นโ€˜(๐‘ ยท ๐‘Œ)))
2219, 21opeq12d 3798 . . . . . . . . . . 11 (๐‘ž = ๐‘Œ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ)
2322sneqd 3617 . . . . . . . . . 10 (๐‘ž = ๐‘Œ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} = {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ})
2423ssiun2s 3942 . . . . . . . . 9 (๐‘Œ โˆˆ ๐‘‰ โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2524ralrimivw 2561 . . . . . . . 8 (๐‘Œ โˆˆ ๐‘‰ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
26 ss2iun 3913 . . . . . . . 8 (โˆ€๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2725, 26syl 14 . . . . . . 7 (๐‘Œ โˆˆ ๐‘‰ โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
28273ad2ant3 1021 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โˆช ๐‘ โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2917, 28sstrd 3177 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
3043ad2ant1 1019 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
3129, 30sseqtrrd 3206 . . . 4 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ )
32 fof 5450 . . . . . . . . . . 11 (๐น:๐‘‰โ€“ontoโ†’๐ต โ†’ ๐น:๐‘‰โŸถ๐ต)
332, 32syl 14 . . . . . . . . . 10 (๐œ‘ โ†’ ๐น:๐‘‰โŸถ๐ต)
34333ad2ant1 1019 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐น:๐‘‰โŸถ๐ต)
3553ad2ant1 1019 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐‘‰ โˆˆ ๐‘Š)
3634, 35fexd 5759 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐น โˆˆ V)
37 simp2 999 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐‘‹ โˆˆ ๐‘‰)
38 fvexg 5546 . . . . . . . 8 ((๐น โˆˆ V โˆง ๐‘‹ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘‹) โˆˆ V)
3936, 37, 38syl2anc 411 . . . . . . 7 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘‹) โˆˆ V)
40 simp3 1000 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ๐‘Œ โˆˆ ๐‘‰)
41 fvexg 5546 . . . . . . . 8 ((๐น โˆˆ V โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘Œ) โˆˆ V)
4236, 40, 41syl2anc 411 . . . . . . 7 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘Œ) โˆˆ V)
43 opexg 4240 . . . . . . 7 (((๐นโ€˜๐‘‹) โˆˆ V โˆง (๐นโ€˜๐‘Œ) โˆˆ V) โ†’ โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ โˆˆ V)
4439, 42, 43syl2anc 411 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ โˆˆ V)
4563ad2ant1 1019 . . . . . . . 8 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ยท โˆˆ ๐ถ)
46 ovexg 5922 . . . . . . . 8 ((๐‘‹ โˆˆ ๐‘‰ โˆง ยท โˆˆ ๐ถ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐‘‹ ยท ๐‘Œ) โˆˆ V)
4737, 45, 40, 46syl3anc 1248 . . . . . . 7 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐‘‹ ยท ๐‘Œ) โˆˆ V)
48 fvexg 5546 . . . . . . 7 ((๐น โˆˆ V โˆง (๐‘‹ ยท ๐‘Œ) โˆˆ V) โ†’ (๐นโ€˜(๐‘‹ ยท ๐‘Œ)) โˆˆ V)
4936, 47, 48syl2anc 411 . . . . . 6 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (๐นโ€˜(๐‘‹ ยท ๐‘Œ)) โˆˆ V)
50 opexg 4240 . . . . . 6 ((โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ โˆˆ V โˆง (๐นโ€˜(๐‘‹ ยท ๐‘Œ)) โˆˆ V) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V)
5144, 49, 50syl2anc 411 . . . . 5 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V)
52 snssg 3738 . . . . 5 (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ V โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ ))
5351, 52syl 14 . . . 4 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ} โІ โˆ™ ))
5431, 53mpbird 167 . . 3 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ )
55 funopfv 5568 . . 3 (Fun โˆ™ โ†’ (โŸจโŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ, (๐นโ€˜(๐‘‹ ยท ๐‘Œ))โŸฉ โˆˆ โˆ™ โ†’ ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ))))
5610, 54, 55sylc 62 . 2 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ( โˆ™ โ€˜โŸจ(๐นโ€˜๐‘‹), (๐นโ€˜๐‘Œ)โŸฉ) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
571, 56eqtrid 2232 1 ((๐œ‘ โˆง ๐‘‹ โˆˆ ๐‘‰ โˆง ๐‘Œ โˆˆ ๐‘‰) โ†’ ((๐นโ€˜๐‘‹) โˆ™ (๐นโ€˜๐‘Œ)) = (๐นโ€˜(๐‘‹ ยท ๐‘Œ)))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 979   = wceq 1363   โˆˆ wcel 2158  โˆ€wral 2465  Vcvv 2749   โІ wss 3141  {csn 3604  โŸจcop 3607  โˆช ciun 3898   ร— cxp 4636  Fun wfun 5222   Fn wfn 5223  โŸถwf 5224  โ€“ontoโ†’wfo 5226  โ€˜cfv 5228  (class class class)co 5888
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-ov 5891
This theorem is referenced by:  imasaddval  12756  imasmulval  12759  qusaddvallemg  12770
  Copyright terms: Public domain W3C validator