Metamath Proof Explorer


Theorem vdwlem4

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem3.v โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ โ„• )
vdwlem3.w โŠข ( ๐œ‘ โ†’ ๐‘Š โˆˆ โ„• )
vdwlem4.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Fin )
vdwlem4.h โŠข ( ๐œ‘ โ†’ ๐ป : ( 1 ... ( ๐‘Š ยท ( 2 ยท ๐‘‰ ) ) ) โŸถ ๐‘… )
vdwlem4.f โŠข ๐น = ( ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) โ†ฆ ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) )
Assertion vdwlem4 ( ๐œ‘ โ†’ ๐น : ( 1 ... ๐‘‰ ) โŸถ ( ๐‘… โ†‘m ( 1 ... ๐‘Š ) ) )

Proof

Step Hyp Ref Expression
1 vdwlem3.v โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ โ„• )
2 vdwlem3.w โŠข ( ๐œ‘ โ†’ ๐‘Š โˆˆ โ„• )
3 vdwlem4.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Fin )
4 vdwlem4.h โŠข ( ๐œ‘ โ†’ ๐ป : ( 1 ... ( ๐‘Š ยท ( 2 ยท ๐‘‰ ) ) ) โŸถ ๐‘… )
5 vdwlem4.f โŠข ๐น = ( ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) โ†ฆ ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) )
6 4 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ๐ป : ( 1 ... ( ๐‘Š ยท ( 2 ยท ๐‘‰ ) ) ) โŸถ ๐‘… )
7 1 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ๐‘‰ โˆˆ โ„• )
8 2 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ๐‘Š โˆˆ โ„• )
9 simplr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) )
10 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) )
11 7 8 9 10 vdwlem3 โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) โˆˆ ( 1 ... ( ๐‘Š ยท ( 2 ยท ๐‘‰ ) ) ) )
12 6 11 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โˆง ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) ) โ†’ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) โˆˆ ๐‘… )
13 12 fmpttd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โ†’ ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) : ( 1 ... ๐‘Š ) โŸถ ๐‘… )
14 3 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โ†’ ๐‘… โˆˆ Fin )
15 ovex โŠข ( 1 ... ๐‘Š ) โˆˆ V
16 elmapg โŠข ( ( ๐‘… โˆˆ Fin โˆง ( 1 ... ๐‘Š ) โˆˆ V ) โ†’ ( ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) โˆˆ ( ๐‘… โ†‘m ( 1 ... ๐‘Š ) ) โ†” ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) : ( 1 ... ๐‘Š ) โŸถ ๐‘… ) )
17 14 15 16 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โ†’ ( ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) โˆˆ ( ๐‘… โ†‘m ( 1 ... ๐‘Š ) ) โ†” ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) : ( 1 ... ๐‘Š ) โŸถ ๐‘… ) )
18 13 17 mpbird โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘‰ ) ) โ†’ ( ๐‘ฆ โˆˆ ( 1 ... ๐‘Š ) โ†ฆ ( ๐ป โ€˜ ( ๐‘ฆ + ( ๐‘Š ยท ( ( ๐‘ฅ โˆ’ 1 ) + ๐‘‰ ) ) ) ) ) โˆˆ ( ๐‘… โ†‘m ( 1 ... ๐‘Š ) ) )
19 18 5 fmptd โŠข ( ๐œ‘ โ†’ ๐น : ( 1 ... ๐‘‰ ) โŸถ ( ๐‘… โ†‘m ( 1 ... ๐‘Š ) ) )