MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwlem10 Structured version   Visualization version   GIF version

Theorem vdwlem10 16923
Description: Lemma for vdw 16927. Set up secondary induction on ๐‘€. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdw.r (๐œ‘ โ†’ ๐‘… โˆˆ Fin)
vdwlem9.k (๐œ‘ โ†’ ๐พ โˆˆ (โ„คโ‰ฅโ€˜2))
vdwlem9.s (๐œ‘ โ†’ โˆ€๐‘  โˆˆ Fin โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“)
vdwlem10.m (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
Assertion
Ref Expression
vdwlem10 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
Distinct variable groups:   ๐œ‘,๐‘›,๐‘“   ๐‘“,๐‘ ,๐พ,๐‘›   ๐‘“,๐‘€,๐‘›   ๐‘…,๐‘“,๐‘›,๐‘    ๐œ‘,๐‘“
Allowed substitution hints:   ๐œ‘(๐‘ )   ๐‘€(๐‘ )

Proof of Theorem vdwlem10
Dummy variables ๐‘Ž ๐‘ ๐‘‘ ๐‘” โ„Ž ๐‘˜ ๐‘š ๐‘ข ๐‘ฃ ๐‘ค ๐‘ฅ ๐‘ฆ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vdwlem10.m . 2 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
2 opeq1 4874 . . . . . . 7 (๐‘ฅ = 1 โ†’ โŸจ๐‘ฅ, ๐พโŸฉ = โŸจ1, ๐พโŸฉ)
32breq1d 5159 . . . . . 6 (๐‘ฅ = 1 โ†’ (โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โ†” โŸจ1, ๐พโŸฉ PolyAP ๐‘“))
43orbi1d 916 . . . . 5 (๐‘ฅ = 1 โ†’ ((โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
54rexralbidv 3221 . . . 4 (๐‘ฅ = 1 โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
65imbi2d 341 . . 3 (๐‘ฅ = 1 โ†’ ((๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)) โ†” (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))))
7 opeq1 4874 . . . . . . 7 (๐‘ฅ = ๐‘š โ†’ โŸจ๐‘ฅ, ๐พโŸฉ = โŸจ๐‘š, ๐พโŸฉ)
87breq1d 5159 . . . . . 6 (๐‘ฅ = ๐‘š โ†’ (โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โ†” โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“))
98orbi1d 916 . . . . 5 (๐‘ฅ = ๐‘š โ†’ ((โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” (โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
109rexralbidv 3221 . . . 4 (๐‘ฅ = ๐‘š โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
1110imbi2d 341 . . 3 (๐‘ฅ = ๐‘š โ†’ ((๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)) โ†” (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))))
12 opeq1 4874 . . . . . . 7 (๐‘ฅ = (๐‘š + 1) โ†’ โŸจ๐‘ฅ, ๐พโŸฉ = โŸจ(๐‘š + 1), ๐พโŸฉ)
1312breq1d 5159 . . . . . 6 (๐‘ฅ = (๐‘š + 1) โ†’ (โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โ†” โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“))
1413orbi1d 916 . . . . 5 (๐‘ฅ = (๐‘š + 1) โ†’ ((โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” (โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
1514rexralbidv 3221 . . . 4 (๐‘ฅ = (๐‘š + 1) โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
1615imbi2d 341 . . 3 (๐‘ฅ = (๐‘š + 1) โ†’ ((๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)) โ†” (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))))
17 opeq1 4874 . . . . . . 7 (๐‘ฅ = ๐‘€ โ†’ โŸจ๐‘ฅ, ๐พโŸฉ = โŸจ๐‘€, ๐พโŸฉ)
1817breq1d 5159 . . . . . 6 (๐‘ฅ = ๐‘€ โ†’ (โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โ†” โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“))
1918orbi1d 916 . . . . 5 (๐‘ฅ = ๐‘€ โ†’ ((โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” (โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
2019rexralbidv 3221 . . . 4 (๐‘ฅ = ๐‘€ โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
2120imbi2d 341 . . 3 (๐‘ฅ = ๐‘€ โ†’ ((๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘ฅ, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)) โ†” (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))))
22 oveq1 7416 . . . . . . . 8 (๐‘  = ๐‘… โ†’ (๐‘  โ†‘m (1...๐‘›)) = (๐‘… โ†‘m (1...๐‘›)))
2322raleqdv 3326 . . . . . . 7 (๐‘  = ๐‘… โ†’ (โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“))
2423rexbidv 3179 . . . . . 6 (๐‘  = ๐‘… โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“))
25 vdwlem9.s . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘  โˆˆ Fin โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“)
26 vdw.r . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ Fin)
2724, 25, 26rspcdva 3614 . . . . 5 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“)
28 oveq2 7417 . . . . . . . 8 (๐‘› = ๐‘ค โ†’ (1...๐‘›) = (1...๐‘ค))
2928oveq2d 7425 . . . . . . 7 (๐‘› = ๐‘ค โ†’ (๐‘… โ†‘m (1...๐‘›)) = (๐‘… โ†‘m (1...๐‘ค)))
3029raleqdv 3326 . . . . . 6 (๐‘› = ๐‘ค โ†’ (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘“))
3130cbvrexvw 3236 . . . . 5 (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆƒ๐‘ค โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘“)
3227, 31sylib 217 . . . 4 (๐œ‘ โ†’ โˆƒ๐‘ค โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘“)
33 breq2 5153 . . . . . . 7 (๐‘“ = ๐‘” โ†’ (๐พ MonoAP ๐‘“ โ†” ๐พ MonoAP ๐‘”))
3433cbvralvw 3235 . . . . . 6 (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘“ โ†” โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘”)
35 2nn 12285 . . . . . . . 8 2 โˆˆ โ„•
36 simpr 486 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ ๐‘ค โˆˆ โ„•)
37 nnmulcl 12236 . . . . . . . 8 ((2 โˆˆ โ„• โˆง ๐‘ค โˆˆ โ„•) โ†’ (2 ยท ๐‘ค) โˆˆ โ„•)
3835, 36, 37sylancr 588 . . . . . . 7 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ (2 ยท ๐‘ค) โˆˆ โ„•)
3926adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ ๐‘… โˆˆ Fin)
40 ovex 7442 . . . . . . . . . . 11 (1...(2 ยท ๐‘ค)) โˆˆ V
41 elmapg 8833 . . . . . . . . . . 11 ((๐‘… โˆˆ Fin โˆง (1...(2 ยท ๐‘ค)) โˆˆ V) โ†’ (๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค))) โ†” ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…))
4239, 40, 41sylancl 587 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ (๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค))) โ†” ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…))
4342biimpa 478 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค)))) โ†’ ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…)
44 simplr 768 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…)
45 elfznn 13530 . . . . . . . . . . . . . . . . . . 19 (๐‘ฆ โˆˆ (1...๐‘ค) โ†’ ๐‘ฆ โˆˆ โ„•)
4645adantl 483 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘ฆ โˆˆ โ„•)
4746nnred 12227 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘ฆ โˆˆ โ„)
48 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘ค โˆˆ โ„•)
4948nnred 12227 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘ค โˆˆ โ„)
50 elfzle2 13505 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ (1...๐‘ค) โ†’ ๐‘ฆ โ‰ค ๐‘ค)
5150adantl 483 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘ฆ โ‰ค ๐‘ค)
5247, 49, 49, 51leadd1dd 11828 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (๐‘ฆ + ๐‘ค) โ‰ค (๐‘ค + ๐‘ค))
5348nncnd 12228 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ๐‘ค โˆˆ โ„‚)
54532timesd 12455 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (2 ยท ๐‘ค) = (๐‘ค + ๐‘ค))
5552, 54breqtrrd 5177 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (๐‘ฆ + ๐‘ค) โ‰ค (2 ยท ๐‘ค))
5646, 48nnaddcld 12264 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (๐‘ฆ + ๐‘ค) โˆˆ โ„•)
57 nnuz 12865 . . . . . . . . . . . . . . . . 17 โ„• = (โ„คโ‰ฅโ€˜1)
5856, 57eleqtrdi 2844 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (๐‘ฆ + ๐‘ค) โˆˆ (โ„คโ‰ฅโ€˜1))
5938ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (2 ยท ๐‘ค) โˆˆ โ„•)
6059nnzd 12585 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (2 ยท ๐‘ค) โˆˆ โ„ค)
61 elfz5 13493 . . . . . . . . . . . . . . . 16 (((๐‘ฆ + ๐‘ค) โˆˆ (โ„คโ‰ฅโ€˜1) โˆง (2 ยท ๐‘ค) โˆˆ โ„ค) โ†’ ((๐‘ฆ + ๐‘ค) โˆˆ (1...(2 ยท ๐‘ค)) โ†” (๐‘ฆ + ๐‘ค) โ‰ค (2 ยท ๐‘ค)))
6258, 60, 61syl2anc 585 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ ((๐‘ฆ + ๐‘ค) โˆˆ (1...(2 ยท ๐‘ค)) โ†” (๐‘ฆ + ๐‘ค) โ‰ค (2 ยท ๐‘ค)))
6355, 62mpbird 257 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (๐‘ฆ + ๐‘ค) โˆˆ (1...(2 ยท ๐‘ค)))
6444, 63ffvelcdmd 7088 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ๐‘ฆ โˆˆ (1...๐‘ค)) โ†’ (๐‘“โ€˜(๐‘ฆ + ๐‘ค)) โˆˆ ๐‘…)
65 fvoveq1 7432 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘“โ€˜(๐‘ฅ + ๐‘ค)) = (๐‘“โ€˜(๐‘ฆ + ๐‘ค)))
6665cbvmptv 5262 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) = (๐‘ฆ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฆ + ๐‘ค)))
6764, 66fmptd 7114 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))):(1...๐‘ค)โŸถ๐‘…)
68 ovex 7442 . . . . . . . . . . . . . 14 (1...๐‘ค) โˆˆ V
69 elmapg 8833 . . . . . . . . . . . . . 14 ((๐‘… โˆˆ Fin โˆง (1...๐‘ค) โˆˆ V) โ†’ ((๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โˆˆ (๐‘… โ†‘m (1...๐‘ค)) โ†” (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))):(1...๐‘ค)โŸถ๐‘…))
7039, 68, 69sylancl 587 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ ((๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โˆˆ (๐‘… โ†‘m (1...๐‘ค)) โ†” (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))):(1...๐‘ค)โŸถ๐‘…))
7170biimpar 479 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))):(1...๐‘ค)โŸถ๐‘…) โ†’ (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โˆˆ (๐‘… โ†‘m (1...๐‘ค)))
7267, 71syldan 592 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โˆˆ (๐‘… โ†‘m (1...๐‘ค)))
73 breq2 5153 . . . . . . . . . . . 12 (๐‘” = (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ†’ (๐พ MonoAP ๐‘” โ†” ๐พ MonoAP (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค)))))
7473rspcv 3609 . . . . . . . . . . 11 ((๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โˆˆ (๐‘… โ†‘m (1...๐‘ค)) โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘” โ†’ ๐พ MonoAP (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค)))))
7572, 74syl 17 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘” โ†’ ๐พ MonoAP (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค)))))
76 2nn0 12489 . . . . . . . . . . . . 13 2 โˆˆ โ„•0
77 vdwlem9.k . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐พ โˆˆ (โ„คโ‰ฅโ€˜2))
7877ad2antrr 725 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ ๐พ โˆˆ (โ„คโ‰ฅโ€˜2))
79 eluznn0 12901 . . . . . . . . . . . . 13 ((2 โˆˆ โ„•0 โˆง ๐พ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐พ โˆˆ โ„•0)
8076, 78, 79sylancr 588 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ ๐พ โˆˆ โ„•0)
8168, 80, 67vdwmc 16911 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (๐พ MonoAP (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ†” โˆƒ๐‘โˆƒ๐‘Ž โˆˆ โ„• โˆƒ๐‘‘ โˆˆ โ„• (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘})))
8239ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ ๐‘… โˆˆ Fin)
8378adantr 482 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ ๐พ โˆˆ (โ„คโ‰ฅโ€˜2))
84 simpllr 775 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ ๐‘ค โˆˆ โ„•)
85 simplr 768 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…)
86 vex 3479 . . . . . . . . . . . . . . . 16 ๐‘ โˆˆ V
87 simprll 778 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ ๐‘Ž โˆˆ โ„•)
88 simprlr 779 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ ๐‘‘ โˆˆ โ„•)
89 simprr 772 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))
9082, 83, 84, 85, 86, 87, 88, 89, 66vdwlem8 16921 . . . . . . . . . . . . . . 15 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ โŸจ1, ๐พโŸฉ PolyAP ๐‘“)
9190orcd 872 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง ((๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•) โˆง (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}))) โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
9291expr 458 . . . . . . . . . . . . 13 ((((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โˆง (๐‘Ž โˆˆ โ„• โˆง ๐‘‘ โˆˆ โ„•)) โ†’ ((๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}) โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
9392rexlimdvva 3212 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (โˆƒ๐‘Ž โˆˆ โ„• โˆƒ๐‘‘ โˆˆ โ„• (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}) โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
9493exlimdv 1937 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (โˆƒ๐‘โˆƒ๐‘Ž โˆˆ โ„• โˆƒ๐‘‘ โˆˆ โ„• (๐‘Ž(APโ€˜๐พ)๐‘‘) โŠ† (โ—ก(๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ€œ {๐‘}) โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
9581, 94sylbid 239 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (๐พ MonoAP (๐‘ฅ โˆˆ (1...๐‘ค) โ†ฆ (๐‘“โ€˜(๐‘ฅ + ๐‘ค))) โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
9675, 95syld 47 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“:(1...(2 ยท ๐‘ค))โŸถ๐‘…) โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘” โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
9743, 96syldan 592 . . . . . . . 8 (((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โˆง ๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค)))) โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘” โ†’ (โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
9897ralrimdva 3155 . . . . . . 7 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘” โ†’ โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค)))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
99 oveq2 7417 . . . . . . . . . 10 (๐‘› = (2 ยท ๐‘ค) โ†’ (1...๐‘›) = (1...(2 ยท ๐‘ค)))
10099oveq2d 7425 . . . . . . . . 9 (๐‘› = (2 ยท ๐‘ค) โ†’ (๐‘… โ†‘m (1...๐‘›)) = (๐‘… โ†‘m (1...(2 ยท ๐‘ค))))
101100raleqdv 3326 . . . . . . . 8 (๐‘› = (2 ยท ๐‘ค) โ†’ (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค)))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
102101rspcev 3613 . . . . . . 7 (((2 ยท ๐‘ค) โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...(2 ยท ๐‘ค)))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
10338, 98, 102syl6an 683 . . . . . 6 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘” โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
10434, 103biimtrid 241 . . . . 5 ((๐œ‘ โˆง ๐‘ค โˆˆ โ„•) โ†’ (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘“ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
105104rexlimdva 3156 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘ค โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘ค))๐พ MonoAP ๐‘“ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
10632, 105mpd 15 . . 3 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ1, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
107 breq2 5153 . . . . . . . . . 10 (๐‘“ = ๐‘” โ†’ (โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โ†” โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘”))
108 breq2 5153 . . . . . . . . . 10 (๐‘“ = ๐‘” โ†’ ((๐พ + 1) MonoAP ๐‘“ โ†” (๐พ + 1) MonoAP ๐‘”))
109107, 108orbi12d 918 . . . . . . . . 9 (๐‘“ = ๐‘” โ†’ ((โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” (โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)))
110109cbvralvw 3235 . . . . . . . 8 (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))
11129raleqdv 3326 . . . . . . . 8 (๐‘› = ๐‘ค โ†’ (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”) โ†” โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)))
112110, 111bitrid 283 . . . . . . 7 (๐‘› = ๐‘ค โ†’ (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)))
113112cbvrexvw 3236 . . . . . 6 (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆƒ๐‘ค โˆˆ โ„• โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))
114 oveq2 7417 . . . . . . . . . . . . 13 (๐‘› = ๐‘ฃ โ†’ (1...๐‘›) = (1...๐‘ฃ))
115114oveq2d 7425 . . . . . . . . . . . 12 (๐‘› = ๐‘ฃ โ†’ (๐‘  โ†‘m (1...๐‘›)) = (๐‘  โ†‘m (1...๐‘ฃ)))
116115raleqdv 3326 . . . . . . . . . . 11 (๐‘› = ๐‘ฃ โ†’ (โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))
117116cbvrexvw 3236 . . . . . . . . . 10 (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆƒ๐‘ฃ โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)
118 oveq1 7416 . . . . . . . . . . . 12 (๐‘  = (๐‘… โ†‘m (1...๐‘ค)) โ†’ (๐‘  โ†‘m (1...๐‘ฃ)) = ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ)))
119118raleqdv 3326 . . . . . . . . . . 11 (๐‘  = (๐‘… โ†‘m (1...๐‘ค)) โ†’ (โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“ โ†” โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))
120119rexbidv 3179 . . . . . . . . . 10 (๐‘  = (๐‘… โ†‘m (1...๐‘ค)) โ†’ (โˆƒ๐‘ฃ โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“ โ†” โˆƒ๐‘ฃ โˆˆ โ„• โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))
121117, 120bitrid 283 . . . . . . . . 9 (๐‘  = (๐‘… โ†‘m (1...๐‘ค)) โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“ โ†” โˆƒ๐‘ฃ โˆˆ โ„• โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))
12225ad2antrr 725 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))) โ†’ โˆ€๐‘  โˆˆ Fin โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“)
12326ad2antrr 725 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))) โ†’ ๐‘… โˆˆ Fin)
124 fzfi 13937 . . . . . . . . . 10 (1...๐‘ค) โˆˆ Fin
125 mapfi 9348 . . . . . . . . . 10 ((๐‘… โˆˆ Fin โˆง (1...๐‘ค) โˆˆ Fin) โ†’ (๐‘… โ†‘m (1...๐‘ค)) โˆˆ Fin)
126123, 124, 125sylancl 587 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))) โ†’ (๐‘… โ†‘m (1...๐‘ค)) โˆˆ Fin)
127121, 122, 126rspcdva 3614 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))) โ†’ โˆƒ๐‘ฃ โˆˆ โ„• โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)
128 simprll 778 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))) โ†’ ๐‘ค โˆˆ โ„•)
129 simprrl 780 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))) โ†’ ๐‘ฃ โˆˆ โ„•)
130 nnmulcl 12236 . . . . . . . . . . . . 13 ((2 โˆˆ โ„• โˆง ๐‘ฃ โˆˆ โ„•) โ†’ (2 ยท ๐‘ฃ) โˆˆ โ„•)
13135, 130mpan 689 . . . . . . . . . . . 12 (๐‘ฃ โˆˆ โ„• โ†’ (2 ยท ๐‘ฃ) โˆˆ โ„•)
132 nnmulcl 12236 . . . . . . . . . . . 12 ((๐‘ค โˆˆ โ„• โˆง (2 ยท ๐‘ฃ) โˆˆ โ„•) โ†’ (๐‘ค ยท (2 ยท ๐‘ฃ)) โˆˆ โ„•)
133131, 132sylan2 594 . . . . . . . . . . 11 ((๐‘ค โˆˆ โ„• โˆง ๐‘ฃ โˆˆ โ„•) โ†’ (๐‘ค ยท (2 ยท ๐‘ฃ)) โˆˆ โ„•)
134128, 129, 133syl2anc 585 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))) โ†’ (๐‘ค ยท (2 ยท ๐‘ฃ)) โˆˆ โ„•)
135 simp1l 1198 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ ๐œ‘)
136135, 26syl 17 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ ๐‘… โˆˆ Fin)
137135, 77syl 17 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ ๐พ โˆˆ (โ„คโ‰ฅโ€˜2))
138135, 25syl 17 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ โˆ€๐‘  โˆˆ Fin โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘  โ†‘m (1...๐‘›))๐พ MonoAP ๐‘“)
139 simp1r 1199 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ ๐‘š โˆˆ โ„•)
140 simp2ll 1241 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ ๐‘ค โˆˆ โ„•)
141 simp2lr 1242 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))
142 breq2 5153 . . . . . . . . . . . . . . . 16 (๐‘” = ๐‘˜ โ†’ (โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โ†” โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘˜))
143 breq2 5153 . . . . . . . . . . . . . . . 16 (๐‘” = ๐‘˜ โ†’ ((๐พ + 1) MonoAP ๐‘” โ†” (๐พ + 1) MonoAP ๐‘˜))
144142, 143orbi12d 918 . . . . . . . . . . . . . . 15 (๐‘” = ๐‘˜ โ†’ ((โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”) โ†” (โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘˜ โˆจ (๐พ + 1) MonoAP ๐‘˜)))
145144cbvralvw 3235 . . . . . . . . . . . . . 14 (โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”) โ†” โˆ€๐‘˜ โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘˜ โˆจ (๐พ + 1) MonoAP ๐‘˜))
146141, 145sylib 217 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ โˆ€๐‘˜ โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘˜ โˆจ (๐พ + 1) MonoAP ๐‘˜))
147 simp2rl 1243 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ ๐‘ฃ โˆˆ โ„•)
148 simp2rr 1244 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)
149 simp3 1139 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ)))))
150 ovex 7442 . . . . . . . . . . . . . . 15 (1...(๐‘ค ยท (2 ยท ๐‘ฃ))) โˆˆ V
151 elmapg 8833 . . . . . . . . . . . . . . 15 ((๐‘… โˆˆ Fin โˆง (1...(๐‘ค ยท (2 ยท ๐‘ฃ))) โˆˆ V) โ†’ (โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ)))) โ†” โ„Ž:(1...(๐‘ค ยท (2 ยท ๐‘ฃ)))โŸถ๐‘…))
152136, 150, 151sylancl 587 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ (โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ)))) โ†” โ„Ž:(1...(๐‘ค ยท (2 ยท ๐‘ฃ)))โŸถ๐‘…))
153149, 152mpbid 231 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ โ„Ž:(1...(๐‘ค ยท (2 ยท ๐‘ฃ)))โŸถ๐‘…)
154 fvoveq1 7432 . . . . . . . . . . . . . . . 16 (๐‘ฆ = ๐‘ข โ†’ (โ„Žโ€˜(๐‘ฆ + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ)))) = (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ)))))
155154cbvmptv 5262 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ฆ + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ))))) = (๐‘ข โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ)))))
156 oveq1 7416 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ = ๐‘ง โ†’ (๐‘ฅ โˆ’ 1) = (๐‘ง โˆ’ 1))
157156oveq1d 7424 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ = ๐‘ง โ†’ ((๐‘ฅ โˆ’ 1) + ๐‘ฃ) = ((๐‘ง โˆ’ 1) + ๐‘ฃ))
158157oveq2d 7425 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ = ๐‘ง โ†’ (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ)) = (๐‘ค ยท ((๐‘ง โˆ’ 1) + ๐‘ฃ)))
159158oveq2d 7425 . . . . . . . . . . . . . . . . 17 (๐‘ฅ = ๐‘ง โ†’ (๐‘ข + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ))) = (๐‘ข + (๐‘ค ยท ((๐‘ง โˆ’ 1) + ๐‘ฃ))))
160159fveq2d 6896 . . . . . . . . . . . . . . . 16 (๐‘ฅ = ๐‘ง โ†’ (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ)))) = (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ง โˆ’ 1) + ๐‘ฃ)))))
161160mpteq2dv 5251 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ง โ†’ (๐‘ข โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ))))) = (๐‘ข โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ง โˆ’ 1) + ๐‘ฃ))))))
162155, 161eqtrid 2785 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ง โ†’ (๐‘ฆ โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ฆ + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ))))) = (๐‘ข โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ง โˆ’ 1) + ๐‘ฃ))))))
163162cbvmptv 5262 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (1...๐‘ฃ) โ†ฆ (๐‘ฆ โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ฆ + (๐‘ค ยท ((๐‘ฅ โˆ’ 1) + ๐‘ฃ)))))) = (๐‘ง โˆˆ (1...๐‘ฃ) โ†ฆ (๐‘ข โˆˆ (1...๐‘ค) โ†ฆ (โ„Žโ€˜(๐‘ข + (๐‘ค ยท ((๐‘ง โˆ’ 1) + ๐‘ฃ))))))
164136, 137, 138, 139, 140, 146, 147, 148, 153, 163vdwlem9 16922 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โˆง โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))) โ†’ (โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž))
1651643expia 1122 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))) โ†’ (โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ)))) โ†’ (โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž)))
166165ralrimiv 3146 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))) โ†’ โˆ€โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž))
167 oveq2 7417 . . . . . . . . . . . . . 14 (๐‘› = (๐‘ค ยท (2 ยท ๐‘ฃ)) โ†’ (1...๐‘›) = (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))
168167oveq2d 7425 . . . . . . . . . . . . 13 (๐‘› = (๐‘ค ยท (2 ยท ๐‘ฃ)) โ†’ (๐‘… โ†‘m (1...๐‘›)) = (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ)))))
169168raleqdv 3326 . . . . . . . . . . . 12 (๐‘› = (๐‘ค ยท (2 ยท ๐‘ฃ)) โ†’ (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
170 breq2 5153 . . . . . . . . . . . . . 14 (๐‘“ = โ„Ž โ†’ (โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โ†” โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž))
171 breq2 5153 . . . . . . . . . . . . . 14 (๐‘“ = โ„Ž โ†’ ((๐พ + 1) MonoAP ๐‘“ โ†” (๐พ + 1) MonoAP โ„Ž))
172170, 171orbi12d 918 . . . . . . . . . . . . 13 (๐‘“ = โ„Ž โ†’ ((โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” (โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž)))
173172cbvralvw 3235 . . . . . . . . . . . 12 (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆ€โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž))
174169, 173bitrdi 287 . . . . . . . . . . 11 (๐‘› = (๐‘ค ยท (2 ยท ๐‘ฃ)) โ†’ (โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†” โˆ€โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž)))
175174rspcev 3613 . . . . . . . . . 10 (((๐‘ค ยท (2 ยท ๐‘ฃ)) โˆˆ โ„• โˆง โˆ€โ„Ž โˆˆ (๐‘… โ†‘m (1...(๐‘ค ยท (2 ยท ๐‘ฃ))))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP โ„Ž โˆจ (๐พ + 1) MonoAP โ„Ž)) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
176134, 166, 175syl2anc 585 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ((๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”)) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“))) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
177176anassrs 469 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))) โˆง (๐‘ฃ โˆˆ โ„• โˆง โˆ€๐‘“ โˆˆ ((๐‘… โ†‘m (1...๐‘ค)) โ†‘m (1...๐‘ฃ))๐พ MonoAP ๐‘“)) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
178127, 177rexlimddv 3162 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘ค โˆˆ โ„• โˆง โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”))) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
179178rexlimdvaa 3157 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โ†’ (โˆƒ๐‘ค โˆˆ โ„• โˆ€๐‘” โˆˆ (๐‘… โ†‘m (1...๐‘ค))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘” โˆจ (๐พ + 1) MonoAP ๐‘”) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
180113, 179biimtrid 241 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
181180expcom 415 . . . 4 (๐‘š โˆˆ โ„• โ†’ (๐œ‘ โ†’ (โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“) โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))))
182181a2d 29 . . 3 (๐‘š โˆˆ โ„• โ†’ ((๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘š, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)) โ†’ (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ(๐‘š + 1), ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))))
1836, 11, 16, 21, 106, 182nnind 12230 . 2 (๐‘€ โˆˆ โ„• โ†’ (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“)))
1841, 183mpcom 38 1 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ โ„• โˆ€๐‘“ โˆˆ (๐‘… โ†‘m (1...๐‘›))(โŸจ๐‘€, ๐พโŸฉ PolyAP ๐‘“ โˆจ (๐พ + 1) MonoAP ๐‘“))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107  โˆ€wral 3062  โˆƒwrex 3071  Vcvv 3475   โŠ† wss 3949  {csn 4629  โŸจcop 4635   class class class wbr 5149   โ†ฆ cmpt 5232  โ—กccnv 5676   โ€œ cima 5680  โŸถwf 6540  โ€˜cfv 6544  (class class class)co 7409   โ†‘m cmap 8820  Fincfn 8939  1c1 11111   + caddc 11113   ยท cmul 11115   โ‰ค cle 11249   โˆ’ cmin 11444  โ„•cn 12212  2c2 12267  โ„•0cn0 12472  โ„คcz 12558  โ„คโ‰ฅcuz 12822  ...cfz 13484  APcvdwa 16898   MonoAP cvdwm 16899   PolyAP cvdwp 16900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-fz 13485  df-hash 14291  df-vdwap 16901  df-vdwmc 16902  df-vdwpc 16903
This theorem is referenced by:  vdwlem11  16924
  Copyright terms: Public domain W3C validator