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

Theorem imasaddfnlemg 12752
Description: The image structure operation is a function if the original operation is compatible with the 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
imasaddfnlemg (๐œ‘ โ†’ โˆ™ Fn (๐ต ร— ๐ต))
Distinct variable groups:   ๐‘ž,๐‘,๐ต   ๐‘Ž,๐‘,๐‘,๐‘ž,๐‘‰   ยท ,๐‘,๐‘ž   ๐น,๐‘Ž,๐‘,๐‘,๐‘ž   ๐œ‘,๐‘Ž,๐‘,๐‘,๐‘ž   โˆ™ ,๐‘Ž,๐‘,๐‘,๐‘ž
Allowed substitution hints:   ๐ต(๐‘Ž,๐‘)   ๐ถ(๐‘ž,๐‘,๐‘Ž,๐‘)   ยท (๐‘Ž,๐‘)   ๐‘Š(๐‘ž,๐‘,๐‘Ž,๐‘)

Proof of Theorem imasaddfnlemg
Dummy variables ๐‘ค ๐‘ฆ ๐‘ง ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasaddf.f . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐น:๐‘‰โ€“ontoโ†’๐ต)
2 fof 5450 . . . . . . . . . . . . 13 (๐น:๐‘‰โ€“ontoโ†’๐ต โ†’ ๐น:๐‘‰โŸถ๐ต)
31, 2syl 14 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐น:๐‘‰โŸถ๐ต)
4 imasaddfnlemg.v . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‰ โˆˆ ๐‘Š)
53, 4fexd 5759 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐น โˆˆ V)
6 vex 2752 . . . . . . . . . . 11 ๐‘ โˆˆ V
7 fvexg 5546 . . . . . . . . . . 11 ((๐น โˆˆ V โˆง ๐‘ โˆˆ V) โ†’ (๐นโ€˜๐‘) โˆˆ V)
85, 6, 7sylancl 413 . . . . . . . . . 10 (๐œ‘ โ†’ (๐นโ€˜๐‘) โˆˆ V)
9 vex 2752 . . . . . . . . . . 11 ๐‘ž โˆˆ V
10 fvexg 5546 . . . . . . . . . . 11 ((๐น โˆˆ V โˆง ๐‘ž โˆˆ V) โ†’ (๐นโ€˜๐‘ž) โˆˆ V)
115, 9, 10sylancl 413 . . . . . . . . . 10 (๐œ‘ โ†’ (๐นโ€˜๐‘ž) โˆˆ V)
12 opexg 4240 . . . . . . . . . 10 (((๐นโ€˜๐‘) โˆˆ V โˆง (๐นโ€˜๐‘ž) โˆˆ V) โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ V)
138, 11, 12syl2anc 411 . . . . . . . . 9 (๐œ‘ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ V)
14 imasaddfnlemg.x . . . . . . . . . . 11 (๐œ‘ โ†’ ยท โˆˆ ๐ถ)
159a1i 9 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ž โˆˆ V)
16 ovexg 5922 . . . . . . . . . . 11 ((๐‘ โˆˆ V โˆง ยท โˆˆ ๐ถ โˆง ๐‘ž โˆˆ V) โ†’ (๐‘ ยท ๐‘ž) โˆˆ V)
176, 14, 15, 16mp3an2i 1352 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ ยท ๐‘ž) โˆˆ V)
18 fvexg 5546 . . . . . . . . . 10 ((๐น โˆˆ V โˆง (๐‘ ยท ๐‘ž) โˆˆ V) โ†’ (๐นโ€˜(๐‘ ยท ๐‘ž)) โˆˆ V)
195, 17, 18syl2anc 411 . . . . . . . . 9 (๐œ‘ โ†’ (๐นโ€˜(๐‘ ยท ๐‘ž)) โˆˆ V)
20 relsnopg 4742 . . . . . . . . 9 ((โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ V โˆง (๐นโ€˜(๐‘ ยท ๐‘ž)) โˆˆ V) โ†’ Rel {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2113, 19, 20syl2anc 411 . . . . . . . 8 (๐œ‘ โ†’ Rel {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2221ralrimivw 2561 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ž โˆˆ ๐‘‰ Rel {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
23 reliun 4759 . . . . . . 7 (Rel โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โˆ€๐‘ž โˆˆ ๐‘‰ Rel {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2422, 23sylibr 134 . . . . . 6 (๐œ‘ โ†’ Rel โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2524ralrimivw 2561 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ Rel โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
26 reliun 4759 . . . . 5 (Rel โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โˆ€๐‘ โˆˆ ๐‘‰ Rel โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2725, 26sylibr 134 . . . 4 (๐œ‘ โ†’ Rel โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
28 imasaddflem.a . . . . 5 (๐œ‘ โ†’ โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
2928releqd 4722 . . . 4 (๐œ‘ โ†’ (Rel โˆ™ โ†” Rel โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ}))
3027, 29mpbird 167 . . 3 (๐œ‘ โ†’ Rel โˆ™ )
31 ffvelcdm 5662 . . . . . . . . . . . . . . . 16 ((๐น:๐‘‰โŸถ๐ต โˆง ๐‘ โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘) โˆˆ ๐ต)
32 ffvelcdm 5662 . . . . . . . . . . . . . . . 16 ((๐น:๐‘‰โŸถ๐ต โˆง ๐‘ž โˆˆ ๐‘‰) โ†’ (๐นโ€˜๐‘ž) โˆˆ ๐ต)
3331, 32anim12dan 600 . . . . . . . . . . . . . . 15 ((๐น:๐‘‰โŸถ๐ต โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ ((๐นโ€˜๐‘) โˆˆ ๐ต โˆง (๐นโ€˜๐‘ž) โˆˆ ๐ต))
343, 33sylan 283 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ ((๐นโ€˜๐‘) โˆˆ ๐ต โˆง (๐นโ€˜๐‘ž) โˆˆ ๐ต))
35 opelxpi 4670 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘) โˆˆ ๐ต โˆง (๐นโ€˜๐‘ž) โˆˆ ๐ต) โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ (๐ต ร— ๐ต))
3634, 35syl 14 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ (๐ต ร— ๐ต))
3719adantr 276 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (๐นโ€˜(๐‘ ยท ๐‘ž)) โˆˆ V)
3836, 37opelxpd 4671 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ ((๐ต ร— ๐ต) ร— V))
3938snssd 3749 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ ((๐ต ร— ๐ต) ร— V))
4039anassrs 400 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ โˆˆ ๐‘‰) โˆง ๐‘ž โˆˆ ๐‘‰) โ†’ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ ((๐ต ร— ๐ต) ร— V))
4140iunssd 3944 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ ๐‘‰) โ†’ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ ((๐ต ร— ๐ต) ร— V))
4241iunssd 3944 . . . . . . . 8 (๐œ‘ โ†’ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ ((๐ต ร— ๐ต) ร— V))
4328, 42eqsstrd 3203 . . . . . . 7 (๐œ‘ โ†’ โˆ™ โІ ((๐ต ร— ๐ต) ร— V))
44 dmss 4838 . . . . . . 7 ( โˆ™ โІ ((๐ต ร— ๐ต) ร— V) โ†’ dom โˆ™ โІ dom ((๐ต ร— ๐ต) ร— V))
4543, 44syl 14 . . . . . 6 (๐œ‘ โ†’ dom โˆ™ โІ dom ((๐ต ร— ๐ต) ร— V))
46 vn0m 3446 . . . . . . 7 โˆƒ๐‘ค ๐‘ค โˆˆ V
47 dmxpm 4859 . . . . . . 7 (โˆƒ๐‘ค ๐‘ค โˆˆ V โ†’ dom ((๐ต ร— ๐ต) ร— V) = (๐ต ร— ๐ต))
4846, 47ax-mp 5 . . . . . 6 dom ((๐ต ร— ๐ต) ร— V) = (๐ต ร— ๐ต)
4945, 48sseqtrdi 3215 . . . . 5 (๐œ‘ โ†’ dom โˆ™ โІ (๐ต ร— ๐ต))
50 forn 5453 . . . . . . 7 (๐น:๐‘‰โ€“ontoโ†’๐ต โ†’ ran ๐น = ๐ต)
511, 50syl 14 . . . . . 6 (๐œ‘ โ†’ ran ๐น = ๐ต)
5251sqxpeqd 4664 . . . . 5 (๐œ‘ โ†’ (ran ๐น ร— ran ๐น) = (๐ต ร— ๐ต))
5349, 52sseqtrrd 3206 . . . 4 (๐œ‘ โ†’ dom โˆ™ โІ (ran ๐น ร— ran ๐น))
5428eleq2d 2257 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆ™ โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ}))
5554adantr 276 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆ™ โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ}))
56 df-br 4016 . . . . . . . . . . . 12 (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆ™ )
57 eliun 3902 . . . . . . . . . . . . 13 (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โˆƒ๐‘ โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
58 eliun 3902 . . . . . . . . . . . . . 14 (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โˆƒ๐‘ž โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
5958rexbii 2494 . . . . . . . . . . . . 13 (โˆƒ๐‘ โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โˆƒ๐‘ โˆˆ ๐‘‰ โˆƒ๐‘ž โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
6057, 59bitr2i 185 . . . . . . . . . . . 12 (โˆƒ๐‘ โˆˆ ๐‘‰ โˆƒ๐‘ž โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ})
6155, 56, 603bitr4g 223 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค โ†” โˆƒ๐‘ โˆˆ ๐‘‰ โˆƒ๐‘ž โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ}))
62 vex 2752 . . . . . . . . . . . . . . . . . . 19 ๐‘Ž โˆˆ V
63 fvexg 5546 . . . . . . . . . . . . . . . . . . 19 ((๐น โˆˆ V โˆง ๐‘Ž โˆˆ V) โ†’ (๐นโ€˜๐‘Ž) โˆˆ V)
645, 62, 63sylancl 413 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐นโ€˜๐‘Ž) โˆˆ V)
65 vex 2752 . . . . . . . . . . . . . . . . . . 19 ๐‘ โˆˆ V
66 fvexg 5546 . . . . . . . . . . . . . . . . . . 19 ((๐น โˆˆ V โˆง ๐‘ โˆˆ V) โ†’ (๐นโ€˜๐‘) โˆˆ V)
675, 65, 66sylancl 413 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐นโ€˜๐‘) โˆˆ V)
68 opexg 4240 . . . . . . . . . . . . . . . . . 18 (((๐นโ€˜๐‘Ž) โˆˆ V โˆง (๐นโ€˜๐‘) โˆˆ V) โ†’ โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆˆ V)
6964, 67, 68syl2anc 411 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆˆ V)
70 vex 2752 . . . . . . . . . . . . . . . . 17 ๐‘ค โˆˆ V
71 opexg 4240 . . . . . . . . . . . . . . . . 17 ((โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆˆ V โˆง ๐‘ค โˆˆ V) โ†’ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ V)
7269, 70, 71sylancl 413 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ V)
73 elsng 3619 . . . . . . . . . . . . . . . 16 (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ V โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ))
7472, 73syl 14 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ))
75743ad2ant1 1019 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†” โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ))
76 opthg 4250 . . . . . . . . . . . . . . . . 17 ((โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆˆ V โˆง ๐‘ค โˆˆ V) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โ†” (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆง ๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž)))))
7769, 70, 76sylancl 413 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โ†” (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆง ๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž)))))
78773ad2ant1 1019 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โ†” (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆง ๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž)))))
79 opthg 4250 . . . . . . . . . . . . . . . . . . . 20 (((๐นโ€˜๐‘Ž) โˆˆ V โˆง (๐นโ€˜๐‘) โˆˆ V) โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โ†” ((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž))))
8064, 67, 79syl2anc 411 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โ†” ((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž))))
81803ad2ant1 1019 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โ†” ((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž))))
82 imasaddf.e . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (((๐นโ€˜๐‘Ž) = (๐นโ€˜๐‘) โˆง (๐นโ€˜๐‘) = (๐นโ€˜๐‘ž)) โ†’ (๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž))))
8381, 82sylbid 150 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โ†’ (๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž))))
84 eqeq2 2197 . . . . . . . . . . . . . . . . . 18 ((๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž)) โ†’ (๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘)) โ†” ๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž))))
8584biimprd 158 . . . . . . . . . . . . . . . . 17 ((๐นโ€˜(๐‘Ž ยท ๐‘)) = (๐นโ€˜(๐‘ ยท ๐‘ž)) โ†’ (๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž)) โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
8683, 85syl6 33 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โ†’ (๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž)) โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘)))))
8786impd 254 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ ((โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆง ๐‘ค = (๐นโ€˜(๐‘ ยท ๐‘ž))) โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
8878, 87sylbid 150 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ = โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
8975, 88sylbid 150 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
90893expa 1204 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โˆง (๐‘ โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰)) โ†’ (โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
9190rexlimdvva 2612 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โ†’ (โˆƒ๐‘ โˆˆ ๐‘‰ โˆƒ๐‘ž โˆˆ ๐‘‰ โŸจโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ, ๐‘คโŸฉ โˆˆ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
9261, 91sylbid 150 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โ†’ (โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
9392alrimiv 1884 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โ†’ โˆ€๐‘ค(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))))
94 mo2icl 2928 . . . . . . . . 9 (โˆ€๐‘ค(โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค โ†’ ๐‘ค = (๐นโ€˜(๐‘Ž ยท ๐‘))) โ†’ โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค)
9593, 94syl 14 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ โˆˆ ๐‘‰)) โ†’ โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค)
9695ralrimivva 2569 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐‘‰ โˆ€๐‘ โˆˆ ๐‘‰ โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค)
97 fofn 5452 . . . . . . . . . 10 (๐น:๐‘‰โ€“ontoโ†’๐ต โ†’ ๐น Fn ๐‘‰)
981, 97syl 14 . . . . . . . . 9 (๐œ‘ โ†’ ๐น Fn ๐‘‰)
99 opeq2 3791 . . . . . . . . . . . 12 (๐‘ง = (๐นโ€˜๐‘) โ†’ โŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ = โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ)
10099breq1d 4025 . . . . . . . . . . 11 (๐‘ง = (๐นโ€˜๐‘) โ†’ (โŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค))
101100mobidv 2072 . . . . . . . . . 10 (๐‘ง = (๐นโ€˜๐‘) โ†’ (โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค))
102101ralrn 5667 . . . . . . . . 9 (๐น Fn ๐‘‰ โ†’ (โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆ€๐‘ โˆˆ ๐‘‰ โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค))
10398, 102syl 14 . . . . . . . 8 (๐œ‘ โ†’ (โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆ€๐‘ โˆˆ ๐‘‰ โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค))
104103ralbidv 2487 . . . . . . 7 (๐œ‘ โ†’ (โˆ€๐‘Ž โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆ€๐‘Ž โˆˆ ๐‘‰ โˆ€๐‘ โˆˆ ๐‘‰ โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), (๐นโ€˜๐‘)โŸฉ โˆ™ ๐‘ค))
10596, 104mpbird 167 . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘Ž โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค)
106 opeq1 3790 . . . . . . . . . . 11 (๐‘ฆ = (๐นโ€˜๐‘Ž) โ†’ โŸจ๐‘ฆ, ๐‘งโŸฉ = โŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ)
107106breq1d 4025 . . . . . . . . . 10 (๐‘ฆ = (๐นโ€˜๐‘Ž) โ†’ (โŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค))
108107mobidv 2072 . . . . . . . . 9 (๐‘ฆ = (๐นโ€˜๐‘Ž) โ†’ (โˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค))
109108ralbidv 2487 . . . . . . . 8 (๐‘ฆ = (๐นโ€˜๐‘Ž) โ†’ (โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค))
110109ralrn 5667 . . . . . . 7 (๐น Fn ๐‘‰ โ†’ (โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆ€๐‘Ž โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค))
11198, 110syl 14 . . . . . 6 (๐œ‘ โ†’ (โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค โ†” โˆ€๐‘Ž โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ(๐นโ€˜๐‘Ž), ๐‘งโŸฉ โˆ™ ๐‘ค))
112105, 111mpbird 167 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค)
113 breq1 4018 . . . . . . 7 (๐‘ฅ = โŸจ๐‘ฆ, ๐‘งโŸฉ โ†’ (๐‘ฅ โˆ™ ๐‘ค โ†” โŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค))
114113mobidv 2072 . . . . . 6 (๐‘ฅ = โŸจ๐‘ฆ, ๐‘งโŸฉ โ†’ (โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค โ†” โˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค))
115114ralxp 4782 . . . . 5 (โˆ€๐‘ฅ โˆˆ (ran ๐น ร— ran ๐น)โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค โ†” โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโˆƒ*๐‘คโŸจ๐‘ฆ, ๐‘งโŸฉ โˆ™ ๐‘ค)
116112, 115sylibr 134 . . . 4 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ (ran ๐น ร— ran ๐น)โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค)
117 ssralv 3231 . . . 4 (dom โˆ™ โІ (ran ๐น ร— ran ๐น) โ†’ (โˆ€๐‘ฅ โˆˆ (ran ๐น ร— ran ๐น)โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค โ†’ โˆ€๐‘ฅ โˆˆ dom โˆ™ โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค))
11853, 116, 117sylc 62 . . 3 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ dom โˆ™ โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค)
119 dffun7 5255 . . 3 (Fun โˆ™ โ†” (Rel โˆ™ โˆง โˆ€๐‘ฅ โˆˆ dom โˆ™ โˆƒ*๐‘ค ๐‘ฅ โˆ™ ๐‘ค))
12030, 118, 119sylanbrc 417 . 2 (๐œ‘ โ†’ Fun โˆ™ )
121 eqimss2 3222 . . . . . . . . . . 11 ( โˆ™ = โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โ†’ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ )
12228, 121syl 14 . . . . . . . . . 10 (๐œ‘ โ†’ โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ )
123 iunss 3939 . . . . . . . . . 10 (โˆช ๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ โ†” โˆ€๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ )
124122, 123sylib 122 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ )
125 iunss 3939 . . . . . . . . . . 11 (โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ โ†” โˆ€๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ )
126 opexg 4240 . . . . . . . . . . . . . . 15 ((โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ V โˆง (๐นโ€˜(๐‘ ยท ๐‘ž)) โˆˆ V) โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ V)
12713, 19, 126syl2anc 411 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ V)
128 snssg 3738 . . . . . . . . . . . . . 14 (โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ V โ†’ (โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ ))
129127, 128syl 14 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ โˆ™ โ†” {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ ))
130 opeldmg 4844 . . . . . . . . . . . . . 14 ((โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ V โˆง (๐นโ€˜(๐‘ ยท ๐‘ž)) โˆˆ V) โ†’ (โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ โˆ™ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
13113, 19, 130syl2anc 411 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ โˆˆ โˆ™ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
132129, 131sylbird 170 . . . . . . . . . . . 12 (๐œ‘ โ†’ ({โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ โ†’ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
133132ralimdv 2555 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆ€๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ โ†’ โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
134125, 133biimtrid 152 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ โ†’ โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
135134ralimdv 2555 . . . . . . . . 9 (๐œ‘ โ†’ (โˆ€๐‘ โˆˆ ๐‘‰ โˆช ๐‘ž โˆˆ ๐‘‰ {โŸจโŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ, (๐นโ€˜(๐‘ ยท ๐‘ž))โŸฉ} โІ โˆ™ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
136124, 135mpd 13 . . . . . . . 8 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ )
137 opeq2 3791 . . . . . . . . . . . 12 (๐‘ง = (๐นโ€˜๐‘ž) โ†’ โŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ = โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ)
138137eleq1d 2256 . . . . . . . . . . 11 (๐‘ง = (๐นโ€˜๐‘ž) โ†’ (โŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
139138ralrn 5667 . . . . . . . . . 10 (๐น Fn ๐‘‰ โ†’ (โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
14098, 139syl 14 . . . . . . . . 9 (๐œ‘ โ†’ (โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
141140ralbidv 2487 . . . . . . . 8 (๐œ‘ โ†’ (โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ž โˆˆ ๐‘‰ โŸจ(๐นโ€˜๐‘), (๐นโ€˜๐‘ž)โŸฉ โˆˆ dom โˆ™ ))
142136, 141mpbird 167 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ )
143 opeq1 3790 . . . . . . . . . . 11 (๐‘ฆ = (๐นโ€˜๐‘) โ†’ โŸจ๐‘ฆ, ๐‘งโŸฉ = โŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ)
144143eleq1d 2256 . . . . . . . . . 10 (๐‘ฆ = (๐นโ€˜๐‘) โ†’ (โŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ ))
145144ralbidv 2487 . . . . . . . . 9 (๐‘ฆ = (๐นโ€˜๐‘) โ†’ (โˆ€๐‘ง โˆˆ ran ๐นโŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ ))
146145ralrn 5667 . . . . . . . 8 (๐น Fn ๐‘‰ โ†’ (โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ ))
14798, 146syl 14 . . . . . . 7 (๐œ‘ โ†’ (โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ โ†” โˆ€๐‘ โˆˆ ๐‘‰ โˆ€๐‘ง โˆˆ ran ๐นโŸจ(๐นโ€˜๐‘), ๐‘งโŸฉ โˆˆ dom โˆ™ ))
148142, 147mpbird 167 . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ )
149 eleq1 2250 . . . . . . 7 (๐‘ฅ = โŸจ๐‘ฆ, ๐‘งโŸฉ โ†’ (๐‘ฅ โˆˆ dom โˆ™ โ†” โŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ ))
150149ralxp 4782 . . . . . 6 (โˆ€๐‘ฅ โˆˆ (ran ๐น ร— ran ๐น)๐‘ฅ โˆˆ dom โˆ™ โ†” โˆ€๐‘ฆ โˆˆ ran ๐นโˆ€๐‘ง โˆˆ ran ๐นโŸจ๐‘ฆ, ๐‘งโŸฉ โˆˆ dom โˆ™ )
151148, 150sylibr 134 . . . . 5 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ (ran ๐น ร— ran ๐น)๐‘ฅ โˆˆ dom โˆ™ )
152 dfss3 3157 . . . . 5 ((ran ๐น ร— ran ๐น) โІ dom โˆ™ โ†” โˆ€๐‘ฅ โˆˆ (ran ๐น ร— ran ๐น)๐‘ฅ โˆˆ dom โˆ™ )
153151, 152sylibr 134 . . . 4 (๐œ‘ โ†’ (ran ๐น ร— ran ๐น) โІ dom โˆ™ )
15452, 153eqsstrrd 3204 . . 3 (๐œ‘ โ†’ (๐ต ร— ๐ต) โІ dom โˆ™ )
15549, 154eqssd 3184 . 2 (๐œ‘ โ†’ dom โˆ™ = (๐ต ร— ๐ต))
156 df-fn 5231 . 2 ( โˆ™ Fn (๐ต ร— ๐ต) โ†” (Fun โˆ™ โˆง dom โˆ™ = (๐ต ร— ๐ต)))
157120, 155, 156sylanbrc 417 1 (๐œ‘ โ†’ โˆ™ Fn (๐ต ร— ๐ต))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 979  โˆ€wal 1361   = wceq 1363  โˆƒwex 1502  โˆƒ*wmo 2037   โˆˆ wcel 2158  โˆ€wral 2465  โˆƒwrex 2466  Vcvv 2749   โІ wss 3141  {csn 3604  โŸจcop 3607  โˆช ciun 3898   class class class wbr 4015   ร— cxp 4636  dom cdm 4638  ran crn 4639  Rel wrel 4643  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:  imasaddvallemg  12753  imasaddflemg  12754  imasaddfn  12755  imasmulfn  12758
  Copyright terms: Public domain W3C validator