Metamath Proof Explorer


Theorem imasvscafn

Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasvscaf.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ๐น โ€œs ๐‘… ) )
imasvscaf.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( Base โ€˜ ๐‘… ) )
imasvscaf.f โŠข ( ๐œ‘ โ†’ ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต )
imasvscaf.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ ๐‘ )
imasvscaf.g โŠข ๐บ = ( Scalar โ€˜ ๐‘… )
imasvscaf.k โŠข ๐พ = ( Base โ€˜ ๐บ )
imasvscaf.q โŠข ยท = ( ยท๐‘  โ€˜ ๐‘… )
imasvscaf.s โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘ˆ )
imasvscaf.e โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( ( ๐น โ€˜ ๐‘Ž ) = ( ๐น โ€˜ ๐‘ž ) โ†’ ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
Assertion imasvscafn ( ๐œ‘ โ†’ โˆ™ Fn ( ๐พ ร— ๐ต ) )

Proof

Step Hyp Ref Expression
1 imasvscaf.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ๐น โ€œs ๐‘… ) )
2 imasvscaf.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( Base โ€˜ ๐‘… ) )
3 imasvscaf.f โŠข ( ๐œ‘ โ†’ ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต )
4 imasvscaf.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ ๐‘ )
5 imasvscaf.g โŠข ๐บ = ( Scalar โ€˜ ๐‘… )
6 imasvscaf.k โŠข ๐พ = ( Base โ€˜ ๐บ )
7 imasvscaf.q โŠข ยท = ( ยท๐‘  โ€˜ ๐‘… )
8 imasvscaf.s โŠข โˆ™ = ( ยท๐‘  โ€˜ ๐‘ˆ )
9 imasvscaf.e โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( ( ๐น โ€˜ ๐‘Ž ) = ( ๐น โ€˜ ๐‘ž ) โ†’ ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
10 eqid โŠข ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) = ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
11 fvex โŠข ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) โˆˆ V
12 10 11 fnmpoi โŠข ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) Fn ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } )
13 fnrel โŠข ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) Fn ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โ†’ Rel ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
14 12 13 ax-mp โŠข Rel ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
15 14 rgenw โŠข โˆ€ ๐‘ž โˆˆ ๐‘‰ Rel ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
16 reliun โŠข ( Rel โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†” โˆ€ ๐‘ž โˆˆ ๐‘‰ Rel ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
17 15 16 mpbir โŠข Rel โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
18 1 2 3 4 5 6 7 8 imasvsca โŠข ( ๐œ‘ โ†’ โˆ™ = โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
19 18 releqd โŠข ( ๐œ‘ โ†’ ( Rel โˆ™ โ†” Rel โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ) )
20 17 19 mpbiri โŠข ( ๐œ‘ โ†’ Rel โˆ™ )
21 dffn2 โŠข ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) Fn ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โ†” ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) : ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โŸถ V )
22 12 21 mpbi โŠข ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) : ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โŸถ V
23 fssxp โŠข ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) : ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โŸถ V โ†’ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) ร— V ) )
24 22 23 ax-mp โŠข ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) ร— V )
25 fof โŠข ( ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต โ†’ ๐น : ๐‘‰ โŸถ ๐ต )
26 3 25 syl โŠข ( ๐œ‘ โ†’ ๐น : ๐‘‰ โŸถ ๐ต )
27 26 ffvelrnda โŠข ( ( ๐œ‘ โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†’ ( ๐น โ€˜ ๐‘ž ) โˆˆ ๐ต )
28 27 snssd โŠข ( ( ๐œ‘ โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†’ { ( ๐น โ€˜ ๐‘ž ) } โŠ† ๐ต )
29 xpss2 โŠข ( { ( ๐น โ€˜ ๐‘ž ) } โŠ† ๐ต โ†’ ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โŠ† ( ๐พ ร— ๐ต ) )
30 xpss1 โŠข ( ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โŠ† ( ๐พ ร— ๐ต ) โ†’ ( ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) ร— V ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
31 28 29 30 3syl โŠข ( ( ๐œ‘ โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†’ ( ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) ร— V ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
32 24 31 sstrid โŠข ( ( ๐œ‘ โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†’ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
33 32 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
34 iunss โŠข ( โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) โ†” โˆ€ ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
35 33 34 sylibr โŠข ( ๐œ‘ โ†’ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
36 18 35 eqsstrd โŠข ( ๐œ‘ โ†’ โˆ™ โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) )
37 dmss โŠข ( โˆ™ โŠ† ( ( ๐พ ร— ๐ต ) ร— V ) โ†’ dom โˆ™ โŠ† dom ( ( ๐พ ร— ๐ต ) ร— V ) )
38 36 37 syl โŠข ( ๐œ‘ โ†’ dom โˆ™ โŠ† dom ( ( ๐พ ร— ๐ต ) ร— V ) )
39 vn0 โŠข V โ‰  โˆ…
40 dmxp โŠข ( V โ‰  โˆ… โ†’ dom ( ( ๐พ ร— ๐ต ) ร— V ) = ( ๐พ ร— ๐ต ) )
41 39 40 ax-mp โŠข dom ( ( ๐พ ร— ๐ต ) ร— V ) = ( ๐พ ร— ๐ต )
42 38 41 sseqtrdi โŠข ( ๐œ‘ โ†’ dom โˆ™ โŠ† ( ๐พ ร— ๐ต ) )
43 forn โŠข ( ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต โ†’ ran ๐น = ๐ต )
44 3 43 syl โŠข ( ๐œ‘ โ†’ ran ๐น = ๐ต )
45 44 xpeq2d โŠข ( ๐œ‘ โ†’ ( ๐พ ร— ran ๐น ) = ( ๐พ ร— ๐ต ) )
46 42 45 sseqtrrd โŠข ( ๐œ‘ โ†’ dom โˆ™ โŠ† ( ๐พ ร— ran ๐น ) )
47 df-br โŠข ( โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค โ†” โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆ™ )
48 18 eleq2d โŠข ( ๐œ‘ โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆ™ โ†” โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ) )
49 48 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆ™ โ†” โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ) )
50 eliun โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†” โˆƒ ๐‘ž โˆˆ ๐‘‰ โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
51 df-3an โŠข ( ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†” ( ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) โˆง ๐‘ž โˆˆ ๐‘‰ ) )
52 10 mpofun โŠข Fun ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
53 funopfv โŠข ( Fun ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ€˜ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ ) = ๐‘ค ) )
54 52 53 ax-mp โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ€˜ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ ) = ๐‘ค )
55 df-ov โŠข ( ๐‘ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ( ๐น โ€˜ ๐‘Ž ) ) = ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ€˜ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ )
56 opex โŠข โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆˆ V
57 vex โŠข ๐‘ค โˆˆ V
58 56 57 opeldm โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆˆ dom ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) )
59 10 11 dmmpo โŠข dom ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) = ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } )
60 58 59 eleqtrdi โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆˆ ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) )
61 opelxp โŠข ( โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆˆ ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โ†” ( ๐‘ โˆˆ ๐พ โˆง ( ๐น โ€˜ ๐‘Ž ) โˆˆ { ( ๐น โ€˜ ๐‘ž ) } ) )
62 60 61 sylib โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( ๐‘ โˆˆ ๐พ โˆง ( ๐น โ€˜ ๐‘Ž ) โˆˆ { ( ๐น โ€˜ ๐‘ž ) } ) )
63 fvoveq1 โŠข ( ๐‘ง = ๐‘ โ†’ ( ๐น โ€˜ ( ๐‘ง ยท ๐‘ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
64 eqidd โŠข ( ๐‘ฆ = ( ๐น โ€˜ ๐‘Ž ) โ†’ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
65 fvoveq1 โŠข ( ๐‘ = ๐‘ง โ†’ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) = ( ๐น โ€˜ ( ๐‘ง ยท ๐‘ž ) ) )
66 eqidd โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐น โ€˜ ( ๐‘ง ยท ๐‘ž ) ) = ( ๐น โ€˜ ( ๐‘ง ยท ๐‘ž ) ) )
67 65 66 cbvmpov โŠข ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) = ( ๐‘ง โˆˆ ๐พ , ๐‘ฆ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ง ยท ๐‘ž ) ) )
68 63 64 67 11 ovmpo โŠข ( ( ๐‘ โˆˆ ๐พ โˆง ( ๐น โ€˜ ๐‘Ž ) โˆˆ { ( ๐น โ€˜ ๐‘ž ) } ) โ†’ ( ๐‘ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ( ๐น โ€˜ ๐‘Ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
69 62 68 syl โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( ๐‘ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ( ๐น โ€˜ ๐‘Ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
70 55 69 eqtr3id โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ€˜ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
71 54 70 eqtr3d โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
72 71 adantl โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โˆง โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
73 elsni โŠข ( ( ๐น โ€˜ ๐‘Ž ) โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†’ ( ๐น โ€˜ ๐‘Ž ) = ( ๐น โ€˜ ๐‘ž ) )
74 62 73 simpl2im โŠข ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ( ๐น โ€˜ ๐‘Ž ) = ( ๐น โ€˜ ๐‘ž ) )
75 9 74 impel โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โˆง โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ) โ†’ ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) = ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) )
76 72 75 eqtr4d โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โˆง โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) )
77 76 ex โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
78 51 77 sylan2br โŠข ( ( ๐œ‘ โˆง ( ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
79 78 anassrs โŠข ( ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
80 79 rexlimdva โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ ( โˆƒ ๐‘ž โˆˆ ๐‘‰ โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
81 50 80 syl5bi โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
82 49 81 sylbid โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ ( โŸจ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ , ๐‘ค โŸฉ โˆˆ โˆ™ โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
83 47 82 syl5bi โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ ( โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
84 83 alrimiv โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ โˆ€ ๐‘ค ( โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) )
85 mo2icl โŠข ( โˆ€ ๐‘ค ( โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค โ†’ ๐‘ค = ( ๐น โ€˜ ( ๐‘ ยท ๐‘Ž ) ) ) โ†’ โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค )
86 84 85 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘Ž โˆˆ ๐‘‰ ) ) โ†’ โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค )
87 86 ralrimivva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘Ž โˆˆ ๐‘‰ โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค )
88 fofn โŠข ( ๐น : ๐‘‰ โ€“ontoโ†’ ๐ต โ†’ ๐น Fn ๐‘‰ )
89 opeq2 โŠข ( ๐‘ฆ = ( ๐น โ€˜ ๐‘Ž ) โ†’ โŸจ ๐‘ , ๐‘ฆ โŸฉ = โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ )
90 89 breq1d โŠข ( ๐‘ฆ = ( ๐น โ€˜ ๐‘Ž ) โ†’ ( โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค โ†” โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค ) )
91 90 mobidv โŠข ( ๐‘ฆ = ( ๐น โ€˜ ๐‘Ž ) โ†’ ( โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค โ†” โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค ) )
92 91 ralrn โŠข ( ๐น Fn ๐‘‰ โ†’ ( โˆ€ ๐‘ฆ โˆˆ ran ๐น โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค โ†” โˆ€ ๐‘Ž โˆˆ ๐‘‰ โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค ) )
93 3 88 92 3syl โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ฆ โˆˆ ran ๐น โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค โ†” โˆ€ ๐‘Ž โˆˆ ๐‘‰ โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค ) )
94 93 ralbidv โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ฆ โˆˆ ran ๐น โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค โ†” โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘Ž โˆˆ ๐‘‰ โˆƒ* ๐‘ค โŸจ ๐‘ , ( ๐น โ€˜ ๐‘Ž ) โŸฉ โˆ™ ๐‘ค ) )
95 87 94 mpbird โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ฆ โˆˆ ran ๐น โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค )
96 breq1 โŠข ( ๐‘ฅ = โŸจ ๐‘ , ๐‘ฆ โŸฉ โ†’ ( ๐‘ฅ โˆ™ ๐‘ค โ†” โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค ) )
97 96 mobidv โŠข ( ๐‘ฅ = โŸจ ๐‘ , ๐‘ฆ โŸฉ โ†’ ( โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค โ†” โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค ) )
98 97 ralxp โŠข ( โˆ€ ๐‘ฅ โˆˆ ( ๐พ ร— ran ๐น ) โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค โ†” โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ฆ โˆˆ ran ๐น โˆƒ* ๐‘ค โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆ™ ๐‘ค )
99 95 98 sylibr โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ( ๐พ ร— ran ๐น ) โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค )
100 ssralv โŠข ( dom โˆ™ โŠ† ( ๐พ ร— ran ๐น ) โ†’ ( โˆ€ ๐‘ฅ โˆˆ ( ๐พ ร— ran ๐น ) โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค โ†’ โˆ€ ๐‘ฅ โˆˆ dom โˆ™ โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค ) )
101 46 99 100 sylc โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ dom โˆ™ โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค )
102 dffun7 โŠข ( Fun โˆ™ โ†” ( Rel โˆ™ โˆง โˆ€ ๐‘ฅ โˆˆ dom โˆ™ โˆƒ* ๐‘ค ๐‘ฅ โˆ™ ๐‘ค ) )
103 20 101 102 sylanbrc โŠข ( ๐œ‘ โ†’ Fun โˆ™ )
104 eqimss2 โŠข ( โˆ™ = โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โ†’ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ )
105 18 104 syl โŠข ( ๐œ‘ โ†’ โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ )
106 iunss โŠข ( โˆช ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ โ†” โˆ€ ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ )
107 105 106 sylib โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ž โˆˆ ๐‘‰ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ )
108 107 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘ž โˆˆ ๐‘‰ ) โ†’ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ )
109 108 adantrl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ )
110 dmss โŠข ( ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† โˆ™ โ†’ dom ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† dom โˆ™ )
111 109 110 syl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ dom ( ๐‘ โˆˆ ๐พ , ๐‘ฅ โˆˆ { ( ๐น โ€˜ ๐‘ž ) } โ†ฆ ( ๐น โ€˜ ( ๐‘ ยท ๐‘ž ) ) ) โŠ† dom โˆ™ )
112 59 111 eqsstrrid โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) โŠ† dom โˆ™ )
113 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ ๐‘ โˆˆ ๐พ )
114 fvex โŠข ( ๐น โ€˜ ๐‘ž ) โˆˆ V
115 114 snid โŠข ( ๐น โ€˜ ๐‘ž ) โˆˆ { ( ๐น โ€˜ ๐‘ž ) }
116 opelxpi โŠข ( ( ๐‘ โˆˆ ๐พ โˆง ( ๐น โ€˜ ๐‘ž ) โˆˆ { ( ๐น โ€˜ ๐‘ž ) } ) โ†’ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) )
117 113 115 116 sylancl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ ( ๐พ ร— { ( ๐น โ€˜ ๐‘ž ) } ) )
118 112 117 sseldd โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ๐พ โˆง ๐‘ž โˆˆ ๐‘‰ ) ) โ†’ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ dom โˆ™ )
119 118 ralrimivva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ž โˆˆ ๐‘‰ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ dom โˆ™ )
120 opeq2 โŠข ( ๐‘ฆ = ( ๐น โ€˜ ๐‘ž ) โ†’ โŸจ ๐‘ , ๐‘ฆ โŸฉ = โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ )
121 120 eleq1d โŠข ( ๐‘ฆ = ( ๐น โ€˜ ๐‘ž ) โ†’ ( โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ โ†” โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ dom โˆ™ ) )
122 121 ralrn โŠข ( ๐น Fn ๐‘‰ โ†’ ( โˆ€ ๐‘ฆ โˆˆ ran ๐น โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ โ†” โˆ€ ๐‘ž โˆˆ ๐‘‰ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ dom โˆ™ ) )
123 3 88 122 3syl โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ฆ โˆˆ ran ๐น โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ โ†” โˆ€ ๐‘ž โˆˆ ๐‘‰ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ dom โˆ™ ) )
124 123 ralbidv โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ฆ โˆˆ ran ๐น โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ โ†” โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ž โˆˆ ๐‘‰ โŸจ ๐‘ , ( ๐น โ€˜ ๐‘ž ) โŸฉ โˆˆ dom โˆ™ ) )
125 119 124 mpbird โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ฆ โˆˆ ran ๐น โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ )
126 eleq1 โŠข ( ๐‘ฅ = โŸจ ๐‘ , ๐‘ฆ โŸฉ โ†’ ( ๐‘ฅ โˆˆ dom โˆ™ โ†” โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ ) )
127 126 ralxp โŠข ( โˆ€ ๐‘ฅ โˆˆ ( ๐พ ร— ran ๐น ) ๐‘ฅ โˆˆ dom โˆ™ โ†” โˆ€ ๐‘ โˆˆ ๐พ โˆ€ ๐‘ฆ โˆˆ ran ๐น โŸจ ๐‘ , ๐‘ฆ โŸฉ โˆˆ dom โˆ™ )
128 125 127 sylibr โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ( ๐พ ร— ran ๐น ) ๐‘ฅ โˆˆ dom โˆ™ )
129 dfss3 โŠข ( ( ๐พ ร— ran ๐น ) โŠ† dom โˆ™ โ†” โˆ€ ๐‘ฅ โˆˆ ( ๐พ ร— ran ๐น ) ๐‘ฅ โˆˆ dom โˆ™ )
130 128 129 sylibr โŠข ( ๐œ‘ โ†’ ( ๐พ ร— ran ๐น ) โŠ† dom โˆ™ )
131 45 130 eqsstrrd โŠข ( ๐œ‘ โ†’ ( ๐พ ร— ๐ต ) โŠ† dom โˆ™ )
132 42 131 eqssd โŠข ( ๐œ‘ โ†’ dom โˆ™ = ( ๐พ ร— ๐ต ) )
133 df-fn โŠข ( โˆ™ Fn ( ๐พ ร— ๐ต ) โ†” ( Fun โˆ™ โˆง dom โˆ™ = ( ๐พ ร— ๐ต ) ) )
134 103 132 133 sylanbrc โŠข ( ๐œ‘ โ†’ โˆ™ Fn ( ๐พ ร— ๐ต ) )